Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)

Ack-by: SkySkimmer
Reviewed-by: ppedrot

2 files changed, 7 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6f2aeab203..63fbaa6a3b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -571,6 +571,12 @@ let is_primitive env c =
   | Declarations.Primitive _ -> true
   | _ -> false
 
+let get_primitive env c =
+  let cb = lookup_constant c env in
+  match cb.Declarations.const_body with
+  | Declarations.Primitive p -> Some p
+  | _ -> None
+
 let is_int63_type env c =
   match env.retroknowledge.Retroknowledge.retro_int63 with
   | None -> false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index dfd9173d10..414ef2b4d7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -248,6 +248,7 @@ val constant_type_in : env -> Constant.t puniverses -> types
 val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 val is_primitive : env -> Constant.t -> bool
+val get_primitive : env -> Constant.t -> CPrimitives.t option
 
 val is_array_type : env -> Constant.t -> bool
 val is_int63_type : env -> Constant.t -> bool