Module Gensubst

Substitution functions
type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb

The type of functions used for substituting generic arguments.

val substitute : ('raw, 'glb, 'top) Genarg.genarg_type -> 'glb subst_fun
val generic_substitute : Genarg.glob_generic_argument subst_fun
val register_subst0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'glb subst_fun -> unit
val constr_subst : GenConstr.glb subst_fun
val register_constr_subst : (_, 'glb) GenConstr.tag -> 'glb subst_fun -> unit