Module GenConstr

type ('raw, 'glb) tag

Tags for extensible terms. The raw type is contained in constrexpr, and the glb type in glob terms.

val create : string -> (_, _) tag

Create a new tag. Tags should be registered with GlobEnv.register_constr_interp0, Genintern.register_intern_constr, Gensubst.register_constr_subst and Genprint.register_constr_print.

Also optionally

  • Genintern.register_ntn_subst0 (to be used in notations)
  • Genintern.register_intern_pat and Genintern.register_interp_pat (to be used in tactic patterns)
val eq : ('raw1, 'glb1) tag -> ('raw2, 'glb2) tag -> ('raw1 * 'glb1, 'raw2 * 'glb2) Util.eq option
val repr : (_, _) tag -> string
type raw =
| Raw : ('raw, _) tag * 'raw -> raw
type glb =
| Glb : (_, 'glb) tag * 'glb -> glb
module Register (M : sig ... end) : sig ... end