Imported Upstream version 8.5~beta1+dfsg

1 files changed, 40 insertions, 10 deletions

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     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -30,16 +30,25 @@ val add_inline_delta_resolver :
 
 val add_delta_resolver : delta_resolver -> 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