8 files changed, 45 insertions, 22 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 050f986367..b3a4bd7471 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -874,8 +874,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
     (if !dump_bytecode then
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
-  with TooLargeInductive msg ->
-    let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else
+  with TooLargeInductive msg as exn ->
+    let _, info = Exninfo.capture exn in
+    let fn = if fail_on_error then
+        CErrors.user_err ?loc:None ~info ~hdr:"compile"
+      else
         (fun x -> Feedback.msg_warning x) in
     fn msg; None
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d6d52dbc2b..182ed55d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -67,7 +67,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -129,7 +129,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_sprop_allowed = true;
-    env_universes_lbound = Univ.Level.set;
+    env_universes_lbound = UGraph.Bound.Set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7a46538772..79e632daa0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -62,7 +62,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val universes_lbound : env -> Univ.Level.t
-val set_universes_lbound : env -> Univ.Level.t -> env
+val universes_lbound : env -> UGraph.Bound.t
+val set_universes_lbound : env -> UGraph.Bound.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 53fc13b04b..76005a3dc6 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -19,29 +19,27 @@ let is_nan (f : float) = f <> f
 let is_infinity f = f = infinity
 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] 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.
    OCaml prints infinities as "inf" (resp. "-inf")
    but we want "infinity" (resp. "neg_infinity"). *)
-let to_string f =
+let to_string_raw fmt 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
+  else Printf.sprintf fmt f
+
+let to_hex_string = to_string_raw "%h"
+
+(* Printing a binary64 float in 17 decimal places and parsing it again
+   will yield the same float. *)
+let to_string = to_string_raw "%.17g"
 
 let of_string = float_of_string
 
 (* Compiles a float to OCaml code *)
 let compile f =
-  let s =
-    if is_nan f then "nan" else if is_neg_infinity f then "neg_infinity"
-    else Printf.sprintf "%h" f in
-  Printf.sprintf "Float64.of_float (%s)" s
+  Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
 
 let of_float f = f
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index d43ff4553f..0afbfa89da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -19,9 +19,19 @@ val is_nan : t -> bool
 val is_infinity : t -> bool
 val is_neg_infinity : t -> bool
 
-val to_string : t -> string
 val of_string : string -> t
 
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f].  *)
+val to_string : t -> string
+
 val compile : t -> string
 
 val of_float : float -> t
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8ac96a6481..e9687991c0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
       if has_template_poly then
         (* For that particular case, we typecheck the inductive in an environment
            where the universes introduced by the definition are only [>= Prop] *)
-        let env = set_universes_lbound env Univ.Level.prop in
+        let env = set_universes_lbound env UGraph.Bound.Prop in
         push_context_set ~strict:false ctx env
       else
         (* In the regular case, all universes are [> Set] *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5f5f0ef8cd..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -148,8 +148,14 @@ let enforce_leq_alg u v g =
   assert (check_leq g u v);
   cg
 
+module Bound =
+struct
+  type t = Prop | Set
+end
+
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u ~lbound ~strict g =
+  let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
   enforce_constraint (lbound,d,u) {g with graph}
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8d9afb0990..c9fbd7f694 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
+module Bound :
+sig
+  type t = Prop | Set
+  (** The [Prop] bound is only used for template polymorphic inductive types. *)
+end
+
+val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : lbound:Level.t -> AUContext.t check_function
+val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)