diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 71 |
1 files changed, 36 insertions, 35 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 6d86b941..b14d3920 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,15 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** {6 [Mod_subst] } *) open Names -open Term +open Constr (** {6 Delta resolver} *) @@ -20,44 +22,44 @@ type delta_resolver val empty_delta_resolver : delta_resolver val add_mp_delta_resolver : - module_path -> module_path -> delta_resolver -> delta_resolver + ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver val add_kn_delta_resolver : - kernel_name -> kernel_name -> delta_resolver -> delta_resolver + KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * constr 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 *) -val mp_of_delta : delta_resolver -> module_path -> module_path -val kn_of_delta : delta_resolver -> kernel_name -> kernel_name +val mp_of_delta : delta_resolver -> ModPath.t -> ModPath.t +val kn_of_delta : delta_resolver -> KerName.t -> KerName.t (** Build a constant whose canonical part is obtained via a resolver *) -val constant_of_delta_kn : delta_resolver -> kernel_name -> constant +val constant_of_delta_kn : delta_resolver -> KerName.t -> 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 -> kernel_name -> constant + delta_resolver -> delta_resolver -> KerName.t -> Constant.t (** Same for inductive names *) -val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive +val mind_of_delta_kn : delta_resolver -> KerName.t -> MutInd.t val mind_of_deltas_kn : - delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive + delta_resolver -> delta_resolver -> KerName.t -> MutInd.t (** Extract the set of inlined constant in the resolver *) -val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list +val inline_of_delta : int option -> delta_resolver -> (int * KerName.t) list (** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *) -val mp_in_delta : module_path -> delta_resolver -> bool -val con_in_delta : constant -> delta_resolver -> bool -val mind_in_delta : mutual_inductive -> delta_resolver -> bool +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val con_in_delta : Constant.t -> delta_resolver -> bool +val mind_in_delta : MutInd.t -> delta_resolver -> bool (** {6 Substitution} *) @@ -72,15 +74,15 @@ val is_empty_subst : substitution -> bool composition. Most often this is not what you want. For sequential composition, try [join (map_mbid mp delta) subs] **) val add_mbid : - MBId.t -> module_path -> delta_resolver -> substitution -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution -> substitution val add_mp : - module_path -> module_path -> delta_resolver -> substitution -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution -> substitution (** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : - MBId.t -> module_path -> delta_resolver -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution val map_mp : - module_path -> module_path -> delta_resolver -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution (** sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -107,9 +109,9 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted (**/**) (* debugging *) val debug_string_of_subst : substitution -> string -val debug_pr_subst : substitution -> Pp.std_ppcmds +val debug_pr_subst : substitution -> Pp.t val debug_string_of_delta : delta_resolver -> string -val debug_pr_delta : delta_resolver -> Pp.std_ppcmds +val debug_pr_delta : delta_resolver -> Pp.t (**/**) (** [subst_mp sub mp] guarantees that whenever the result of the @@ -117,10 +119,10 @@ val debug_pr_delta : delta_resolver -> Pp.std_ppcmds as well [==] *) val subst_mp : - substitution -> module_path -> module_path + substitution -> ModPath.t -> ModPath.t val subst_mind : - substitution -> mutual_inductive -> mutual_inductive + substitution -> MutInd.t -> MutInd.t val subst_ind : substitution -> inductive -> inductive @@ -128,10 +130,10 @@ val subst_ind : val subst_pind : substitution -> pinductive -> pinductive val subst_kn : - substitution -> kernel_name -> kernel_name + substitution -> KerName.t -> KerName.t val subst_con : - substitution -> pconstant -> constant * constr + substitution -> pconstant -> Constant.t * constr val subst_pcon : substitution -> pconstant -> pconstant @@ -140,10 +142,10 @@ val subst_pcon_term : substitution -> pconstant -> pconstant * constr val subst_con_kn : - substitution -> constant -> constant * constr + substitution -> Constant.t -> Constant.t * constr -val subst_constant : - substitution -> constant -> constant +val subst_constant : + substitution -> Constant.t -> Constant.t (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? @@ -154,7 +156,7 @@ val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) -val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name +val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t (** [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) @@ -171,6 +173,5 @@ val occur_mbid : MBId.t -> substitution -> bool val repr_substituted : 'a substituted -> substitution list option * 'a -val force_constr : Term.constr substituted -> Term.constr -val subst_constr : - substitution -> Term.constr substituted -> Term.constr substituted +val force_constr : constr substituted -> constr +val subst_constr : substitution -> constr substituted -> constr substituted |