3 files changed, 14 insertions, 6 deletions
diff --git a/kernel/float64.ml b/kernel/float64.ml
index 3e36373b77..cc661aeba3 100644
--- a/kernel/float64.ml
+++ b/kernel/float64.ml
@@ -12,7 +12,10 @@
    format *)
 type t = float
 
-let is_nan f = f <> f
+(* The [f : float] type annotation enable the compiler to compile f <> f
+   as comparison on floats rather than the polymorphic OCaml comparison
+   which is much slower. *)
+let is_nan (f : float) = f <> f
 let is_infinity f = f = infinity
 let is_neg_infinity f = f = neg_infinity
 
@@ -42,19 +45,20 @@ let abs = abs_float
 
 type float_comparison = FEq | FLt | FGt | FNotComparable
 
-let eq x y = x = y
+(* See above comment on [is_nan] for the [float] type annotations. *)
+let eq (x : float) (y : float) = x = y
 [@@ocaml.inline always]
 
-let lt x y = x < y
+let lt (x : float) (y : float) = x < y
 [@@ocaml.inline always]
 
-let le x y = x <= y
+let le (x : float) (y : float) = x <= y
 [@@ocaml.inline always]
 
 (* inspired by lib/util.ml; see also #10471 *)
-let pervasives_compare = compare
+let pervasives_compare (x : float) (y : float) = compare x y
 
-let compare x y =
+let compare (x : float) (y : float) =
   if x < y then FLt
   else
   (
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..e8adde2605 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let structure_body_of_safe_env env = env.revstruct
+
 let sections_of_safe_env senv = senv.sections
 
 let get_section = function
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e6f2fc4a5d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
 
 val sections_of_safe_env : safe_environment -> section_data Section.t option
 
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment