Mod_substMod_substA delta resolver is a renaming of kernames and modpaths. Objects on which the resolver acts non-trivially must share a common modpath prefix called the root of the resolver.
val empty_delta_resolver : Names.ModPath.t -> delta_resolverGiven a root, build a resolver.
val has_root_delta_resolver : Names.ModPath.t -> delta_resolver -> boolval add_mp_delta_resolver : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> delta_resolveradd_mp_delta_resolver mp v reso assumes that root(reso) ⊆ mp.
val add_kn_delta_resolver : Names.KerName.t -> Names.KerName.t -> delta_resolver -> delta_resolveradd_kn_delta_resolver kn v reso assumes that root(reso) ⊆ modpath(kn).
val add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr UVars.univ_abstracted option) -> delta_resolver -> delta_resolveradd_inline_delta_resolver kn v reso assumes that root(reso) ⊆ modpath(kn).
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolveradd_delta_resolver reso1 reso2 merges two renamings, assuming that root(reso2) ⊆ root(reso1). Note that this is asymmetrical. The root of the result is root(reso2).
val upcast_delta_resolver : Names.ModPath.t -> delta_resolver -> delta_resolverAssuming mp ⊆ root(delta), upcast_delta_resolver mp delta allows seeing delta as a resolver with root = mp.
Effect 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 for inductive names
val mind_of_delta_kn : 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?
val mp_in_delta : Names.ModPath.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
val subst_mps_list : substitution list -> Constr.constr -> Constr.constr