Module `Mod_subst`

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 Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver

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

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

val mind_of_delta_kn : delta_resolver -> Names.KerName.t -> Names.MutInd.t
val mind_of_deltas_kn : delta_resolver -> 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

val empty_subst : substitution
val is_empty_subst : substitution -> bool
val add_mbid : Names.MBId.t -> Names.ModPath.t -> delta_resolver -> substitution -> substitution: 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 *

val add_mp : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> substitution -> substitution
val map_mbid : Names.MBId.t -> Names.ModPath.t -> delta_resolver -> substitution: map_* create a new substitution arg2/arg1{arg3}

val map_mp : Names.ModPath.t -> Names.ModPath.t -> delta_resolver -> substitution
val join : substitution -> substitution -> substitution: 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

val subst_mp : substitution -> Names.ModPath.t -> Names.ModPath.t
val subst_mind : substitution -> Names.MutInd.t -> Names.MutInd.t
val subst_ind : substitution -> Names.inductive -> Names.inductive
val subst_pind : substitution -> Constr.pinductive -> Constr.pinductive
val subst_kn : substitution -> Names.KerName.t -> Names.KerName.t
val subst_con : substitution -> Names.Constant.t -> Names.Constant.t * Constr.constr Univ.univ_abstracted option
val subst_pcon : substitution -> Constr.pconstant -> Constr.pconstant
val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t
val subst_proj_repr : substitution -> Names.Projection.Repr.t -> Names.Projection.Repr.t
val subst_proj : substitution -> Names.Projection.t -> Names.Projection.t
val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action
val subst_evaluable_reference : substitution -> Names.evaluable_global_reference -> Names.evaluable_global_reference: Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" where X.t is later on instantiated with y? I choose the first interpretation (i.e. an evaluable reference is never expanded).

val replace_mp_in_kn : Names.ModPath.t -> Names.ModPath.t -> Names.KerName.t -> Names.KerName.t: replace_mp_in_con mp mp' con replaces mp with mp' in con

val subst_mps : substitution -> Constr.constr -> Constr.constr: subst_mps sub c performs the substitution sub on all kernel names appearing in c

val repr_substituted : 'a substituted -> substitution list option * 'a
val force_constr : Constr.constr substituted -> Constr.constr
val subst_constr : substitution -> Constr.constr substituted -> Constr.constr substituted