From f724ed1e270eb48060a510ff99219227c342ad6c Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 31 Dec 2020 18:08:29 +0100
Subject: Fix #13579 (hnf on primitives raises an anomaly)

Also works for simpl.
---
 kernel/environ.ml  | 6 ++++++
 kernel/environ.mli | 1 +
 2 files changed, 7 insertions(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3