Merge branch 'v8.5'

7 files changed, 22 insertions, 14 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 9d58f6615..047da682a 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -130,8 +130,8 @@ let key rk =
   match !rk with
   | None -> raise NotEvaluated
   | Some k ->
-      try Ephemeron.get k
-      with Ephemeron.InvalidKey -> raise NotEvaluated
+      try CEphemeron.get k
+      with CEphemeron.InvalidKey -> raise NotEvaluated
 
 (************************)
 (* traduction des patch *)
@@ -170,7 +170,7 @@ let rec slot_for_getglobal env kn =
 	 | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
-    rk := Some (Ephemeron.create pos);
+    rk := Some (CEphemeron.create pos);
     pos
 
 and slot_for_fv env fv =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 3ecfcca64..d07ca2103 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -104,7 +104,7 @@ type side_eff =
   | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
 
 type side_effect = {
-  from_env : Declarations.structure_body Ephemeron.key;
+  from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 229508ea3..551632962 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -794,7 +794,15 @@ let rec subterm_specif renv stack t =
     | Proj (p, c) -> 
       let subt = subterm_specif renv stack c in
 	(match subt with
-	| Subterm (s, wf) -> Subterm (Strict, wf)
+	| Subterm (s, wf) ->
+	   (* We take the subterm specs of the constructor of the record *)
+	   let wf_args = (dest_subterms wf).(0) in
+	   (* We extract the tree of the projected argument *)
+	   let kn = Projection.constant p in
+	   let cb = lookup_constant kn renv.env in
+	   let pb = Option.get cb.const_proj in
+	   let n = pb.proj_arg in
+	   Subterm (Strict, List.nth wf_args n)
 	| Dead_code -> Dead_code
 	| Not_subterm -> Not_subterm)
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 99d99e694..0e56e76aa 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -25,7 +25,7 @@ open Context.Named.Declaration
 (* The key attached to each constant is used by the VM to retrieve previous *)
 (* evaluations of the constant. It is essentially an index in the symbols table *)
 (* used by the VM. *)
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 (** Linking information for the native compiler. *)
 
@@ -50,17 +50,17 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of (values * Id.Set.t) Ephemeron.key
+    | VKvalue of (values * Id.Set.t) CEphemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
 
 let force_lazy_val vk = match !vk with
 | VKnone -> None
-| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None
+| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None
 
 let dummy_lazy_val () = ref VKnone
-let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key)
+let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 
 type named_vals = (Id.t * lazy_val) list
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f626aa0d3..353c46112 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -17,7 +17,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 type constant_key = constant_body * (link_info ref * key)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8a402322f..ce05190b6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -225,11 +225,11 @@ let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEscheme(
       List.map (fun (i,c) ->
         let cbo = Environ.lookup_constant c env.env in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2a3ac957f..3839135a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,14 +125,14 @@ let check_signatures curmb sl =
     | None -> None, None
     | Some curmb ->
         try
-          let mb = Ephemeron.get mb in
+          let mb = CEphemeron.get mb in
           match sl with
           | None -> sl, None
           | Some n ->
               if List.length mb >= how_many && CList.skipn how_many mb == curmb
               then Some (n + how_many), Some mb
               else None, None
-        with Ephemeron.InvalidKey -> None, None in
+        with CEphemeron.InvalidKey -> None, None in
   let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
   sl