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

Ack-by: SkySkimmer
Reviewed-by: ppedrot

1 files changed, 6 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