Mod_substMod_substval empty_delta_resolver : delta_resolverval add_mp_delta_resolver : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> delta_resolverval add_kn_delta_resolver : Names.KerName.t -> Names.KerName.t -> delta_resolver -> delta_resolverval add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr UVars.univ_abstracted option) -> delta_resolver -> delta_resolverval add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolverEffect of a delta_resolver on a module path, on a kernel name
val mp_of_delta : delta_resolver -> Names.ModPath.t -> Names.ModPath.tval kn_of_delta : delta_resolver -> Names.KerName.t -> Names.KerName.tBuild a constant whose canonical part is obtained via a resolver
val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.tSame, but a 2nd resolver is tried if the 1st one had no effect
val constant_of_deltas_kn : delta_resolver -> delta_resolver -> Names.KerName.t -> Names.Constant.tSame for inductive names
val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.tval mind_of_deltas_kn : delta_resolver -> delta_resolver -> Names.KerName.t -> Names.MutInd.tval inline_of_delta : int option -> delta_resolver -> (int * Names.KerName.t) listExtract the set of inlined constant in the resolver
Does a delta_resolver contains a mp, a constant, an inductive ?
val mp_in_delta : Names.ModPath.t -> delta_resolver -> boolval con_in_delta : Names.Constant.t -> delta_resolver -> boolval mind_in_delta : Names.MutInd.t -> delta_resolver -> boolval empty_subst : substitutionval is_empty_subst : substitution -> boolval add_mbid : Names.MBId.t -> Names.ModPath.t -> delta_resolver -> substitution -> substitutionadd_* add arg2/arg1{arg3} to the substitution with no sequential composition. Most often this is not what you want. For sequential composition, try join (map_mbid mp delta) subs *
val add_mp : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> substitution -> substitutionval map_mbid : Names.MBId.t -> Names.ModPath.t -> delta_resolver -> substitutionmap_* create a new substitution arg2/arg1{arg3}
val map_mp : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> substitutionval join : substitution -> substitution -> substitutionsequential composition: substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)
val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolverApply the substitution on the domain of the resolver
val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolverApply the substitution on the codomain of the resolver
val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolversubst_mp sub mp guarantees that whenever the result of the substitution is structutally equal mp, it is equal by pointers as well ==
val subst_mp : substitution -> Names.ModPath.t -> Names.ModPath.tval subst_mind : substitution -> Names.MutInd.t -> Names.MutInd.tval subst_ind : substitution -> Names.inductive -> Names.inductiveval subst_constructor : substitution -> Names.constructor -> Names.constructorval subst_pind : substitution -> Constr.pinductive -> Constr.pinductiveval subst_kn : substitution -> Names.KerName.t -> Names.KerName.tval subst_con : substitution -> Names.Constant.t -> Names.Constant.t * Constr.constr UVars.univ_abstracted optionval subst_pcon : substitution -> Constr.pconstant -> Constr.pconstantval subst_constant : substitution -> Names.Constant.t -> Names.Constant.tval subst_proj_repr : substitution -> Names.Projection.Repr.t -> Names.Projection.Repr.tval subst_proj : substitution -> Names.Projection.t -> Names.Projection.tval subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.actionval replace_mp_in_kn : Names.ModPath.t -> Names.ModPath.t -> Names.KerName.t -> Names.KerName.treplace_mp_in_con mp mp' con replaces mp with mp' in con
val subst_mps : substitution -> Constr.constr -> Constr.constrsubst_mps sub c performs the substitution sub on all kernel names appearing in c