From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/mod_subst.mli | 50 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 40 insertions(+), 10 deletions(-) (limited to 'kernel/mod_subst.mli') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index d29b4c9a..fc2b0441 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* delta_resolver -> delta_resolver -(** Effect of a [delta_resolver] on kernel name, constant, inductive, etc *) +(** 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 + +(** 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 : delta_resolver -> constant -> constant -val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive -val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive +(** Same, but a 2nd resolver is tried if the 1st one had no effect *) -val mp_of_delta : delta_resolver -> module_path -> module_path +val constant_of_deltas_kn : + delta_resolver -> delta_resolver -> kernel_name -> constant + +(** Same for inductive names *) + +val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive +val mind_of_deltas_kn : + delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive (** Extract the set of inlined constant in the resolver *) val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list @@ -62,13 +71,13 @@ val is_empty_subst : substitution -> bool (** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential composition *) val add_mbid : - mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution + MBId.t -> module_path -> delta_resolver -> substitution -> substitution val add_mp : module_path -> module_path -> delta_resolver -> substitution -> substitution (** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : - mod_bound_id -> module_path -> delta_resolver -> substitution + MBId.t -> module_path -> delta_resolver -> substitution val map_mp : module_path -> module_path -> delta_resolver -> substitution @@ -109,15 +118,32 @@ val debug_pr_delta : delta_resolver -> Pp.std_ppcmds val subst_mp : substitution -> module_path -> module_path -val subst_ind : +val subst_mind : substitution -> mutual_inductive -> mutual_inductive +val subst_ind : + substitution -> inductive -> inductive + +val subst_pind : substitution -> pinductive -> pinductive + val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : + substitution -> pconstant -> constant * constr + +val subst_pcon : + substitution -> pconstant -> pconstant + +val subst_pcon_term : + substitution -> pconstant -> pconstant * constr + +val subst_con_kn : substitution -> constant -> constant * constr +val subst_constant : + substitution -> constant -> constant + (** 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" @@ -136,10 +162,14 @@ val subst_mps : substitution -> constr -> constr (** [occur_*id id sub] returns true iff [id] occurs in [sub] on either side *) -val occur_mbid : mod_bound_id -> substitution -> bool +val occur_mbid : MBId.t -> substitution -> bool (** [repr_substituted r] dumps the representation of a substituted: - [None, a] when r is a value - [Some s, a] when r is a delayed substitution [s] applied to [a] *) 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 -- cgit v1.2.3