Module Mod_subst

Delta resolver
type delta_resolver

A delta_resolver maps name (constant, inductive, module_path) to canonical name

val empty_delta_resolver : delta_resolver
val add_mp_delta_resolver : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> delta_resolver
val add_kn_delta_resolver : Names.KerName.t -> Names.KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver : Names.KerName.t -> (int * Constr.constr UVars.univ_abstracted option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

Effect of a delta_resolver on a module path, on a kernel name

Build a constant whose canonical part is obtained via a resolver

val constant_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.Constant.t

Same, 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.t

Same for inductive names

val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
val inline_of_delta : int option -> delta_resolver -> (int * Names.KerName.t) list

Extract 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 -> bool
val con_in_delta : Names.Constant.t -> delta_resolver -> bool
val mind_in_delta : Names.MutInd.t -> delta_resolver -> bool
type substitution
val empty_subst : substitution
val is_empty_subst : substitution -> bool

add_* 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 *

map_* create a new substitution arg2/arg1{arg3}

sequential composition: substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)

val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the domain of the resolver

val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver

Apply the substitution on the codomain of the resolver

val subst_dom_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver

subst_mp sub mp guarantees that whenever the result of the substitution is structutally equal mp, it is equal by pointers as well ==

val subst_constructor : substitution -> Names.constructor -> Names.constructor

replace_mp_in_con mp mp' con replaces mp with mp' in con

subst_mps sub c performs the substitution sub on all kernel names appearing in c

val subst_mps_list : substitution list -> Constr.constr -> Constr.constr