13 files changed, 33 insertions, 15 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/float64.ml b/kernel/float64.ml
index 299f53e8ab..53fc13b04b 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -21,12 +21,19 @@ let is_neg_infinity f = f = neg_infinity
 
 (* Printing a binary64 float in 17 decimal places and parsing it again
    will yield the same float. We assume [to_string_raw] is not given a
-   [nan] as input. *)
+   [nan] or an infinity as input. *)
 let to_string_raw f = Printf.sprintf "%.17g" f
 
 (* OCaml gives a sign to nan values which should not be displayed as
-   all NaNs are considered equal here *)
-let to_string f = if is_nan f then "nan" else to_string_raw f
+   all NaNs are considered equal here.
+   OCaml prints infinities as "inf" (resp. "-inf")
+   but we want "infinity" (resp. "neg_infinity"). *)
+let to_string f =
+  if is_nan f then "nan"
+  else if is_infinity f then "infinity"
+  else if is_neg_infinity f then "neg_infinity"
+  else to_string_raw f
+
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
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
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4c66f1574f..a4465c293b 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -169,9 +169,6 @@ let subst_of_rel_context_instance sign l =
     | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
   in aux [] (List.rev sign) l
 
-let adjust_subst_to_rel_context sign l =
-  List.rev (subst_of_rel_context_instance sign l)
-
 let adjust_rel_to_rel_context sign n =
   let rec aux sign =
     let open RelDecl in
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 52a6159f0a..0aac5ed4ce 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -72,9 +72,6 @@ type substl = constr list
    [c₁], as if usable for [substl]. *)
 val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl
 
-(** For compatibility: returns the substitution reversed *)
-val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list
-
 (** Take an index in an instance of a context and returns its index wrt to
     the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *)
 val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int