Module Gentactic

Generic tactic expressions.

type ('raw, 'glob) tag
val equal : ('raw1, 'glob1) tag -> ('raw2, 'glob2) tag -> ('raw1 * 'glob1, 'raw2 * 'glob2) Util.eq option
val repr : (_, _) tag -> string
type any_tag =
| Any : (_, _) tag -> any_tag
val name : string -> any_tag option
type raw_generic_tactic =
| Raw : ('raw, _) tag * 'raw -> raw_generic_tactic
type glob_generic_tactic =
| Glb : (_, 'glb) tag * 'glb -> glob_generic_tactic
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
module Map (A : sig ... end) : sig ... end