Module Gentactic

Generic tactic expressions.

type raw_generic_tactic
type glob_generic_tactic
type ('raw, 'glob) tag
val make : string -> ('raw, 'glb) tag

Each declared tag must be registered using all the following register functions (except when the callback cannot be called ie when the value type at that level is empty).

val empty : (Util.Empty.t, Util.Empty.t) tag
val of_raw : ('raw, _) tag -> 'raw -> raw_generic_tactic
val register_print : ('raw, 'glb) tag -> 'raw Genprint.printer -> 'glb Genprint.printer -> unit
val register_subst : (_, 'glb) tag -> 'glb Gensubst.subst_fun -> unit
val register_intern : ('raw, 'glb) tag -> ('raw, 'glb) Genintern.intern_fun -> unit
val intern : ?strict:bool -> Environ.env -> ?ltacvars:Names.Id.Set.t -> raw_generic_tactic -> glob_generic_tactic

strict is default true

val register_interp : (_, 'glb) tag -> (Geninterp.Val.t Names.Id.Map.t -> 'glb -> unit Proofview.tactic) -> unit