4 files changed, 8 insertions, 2 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);