Merge PR #9900: [native compiler] Fix critical bug with stuck primitive projections

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 6 insertions, 1 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0b2d760ca8..0003fc7280 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -222,7 +222,12 @@ and nf_type_sort env sigma v =
   match kind_of_value v with
   | Vaccu accu -> 
       let t,s = nf_accu_type env sigma accu in
-      let s = try destSort s with DestKO -> assert false in
+      let s =
+        try
+          destSort (whd_all env s)
+        with DestKO ->
+          CErrors.anomaly (Pp.str "Value should be a sort")
+      in
       t, s
   | _ -> assert false