10 files changed, 23 insertions, 6 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1316dfe069..c31cdae6f5 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -678,6 +678,8 @@ let rec zip m stk =
 
 let fapp_stack (m,stk) = zip m stk
 
+let term_of_process c stk = term_of_fconstr (zip c stk)
+
 (*********************************************************************)
 
 (* The assertions in the functions below are granted because they are
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9e94248113..79092813bc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -227,6 +227,10 @@ val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 val kl : clos_infos -> clos_tab -> fconstr -> constr
 
+val zip : fconstr -> stack -> fconstr
+
+val term_of_process : fconstr -> stack -> constr
+
 val to_constr : lift -> fconstr -> constr
 
 (** End of cbn debug section i*)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d2c9a454b..de8692ff21 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -128,7 +128,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_sprop_allowed = false;
+    env_sprop_allowed = true;
     env_universes_lbound = Univ.Level.set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index dde1274152..494282d4e1 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -37,7 +37,7 @@ let ( / ) = Filename.concat
 let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
 
 let () = at_exit (fun () ->
-    if Lazy.is_val my_temp_dir then
+    if not !Flags.debug && Lazy.is_val my_temp_dir then
       try
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 6cfe44c5ff..a5fcfae1fc 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -96,14 +96,14 @@ let mk_accu (a : atom) : t =
     else
       let data = { data with acc_arg = x :: data.acc_arg } in
       let ans = Obj.repr (accumulate data) in
-      let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
+      let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
       ans
   in
   let acc = { acc_atm = a; acc_arg = [] } in
   let ans = Obj.repr (accumulate acc) in
   (** FIXME: use another representation for accumulators, this causes naked
       pointers. *)
-  let () = Obj.set_tag ans accumulate_tag [@ocaml.alert "--deprecated"] in
+  let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
   (Obj.obj ans : t)
 
 let get_accu (k : accumulator) =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 469d5ccaa2..7574d7b21e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         (match kind a1, kind a2 with
            | (Sort s1, Sort s2) ->
                if not (is_empty_stack v1 && is_empty_stack v2) then
-                 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
+                 (* May happen because we convert application right to left *)
+                 raise NotConvertible;
               sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
            | (Meta n, Meta m) ->
                if Int.equal n m
@@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
-          anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
+          (* May happen because we convert application right to left *)
+          raise NotConvertible;
         (* Luo's system *)
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..50922ffc52 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -301,6 +301,7 @@ sig
   type t
   val repr : t -> side_effect list
   val empty : t
+  val is_empty : t -> bool
   val add : side_effect -> t -> t
   val concat : t -> t -> t
 end =
@@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
 
 let repr eff = eff.seff
 let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
 let add x es =
   if SeffSet.mem x es.elts then es
   else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +351,7 @@ let push_private_constants env eff =
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
 let concat_private = SideEffects.concat
 
 let universes_of_private eff =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f8d5d319a9..b42746a882 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -50,6 +50,8 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 type private_constants
 
 val empty_private_constants : private_constants
+val is_empty_private_constants : private_constants -> bool
+
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
 
 type family = InSProp | InProp | InSet | InType
 
+let all_families = [InSProp; InProp; InSet; InType]
+
 type t =
   | SProp
   | Prop
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
 
 type family = InSProp | InProp | InSet | InType
 
+val all_families : family list
+
 type t = private
   | SProp
   | Prop