From 73e7bbab4ff6120318ec7b90e4971bfafd09cfb5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 00:26:20 +0200
Subject: [native compiler] Normalize before destructuring sort

This was making an assertion fail on
https://github.com/coq/coq/issues/9684 after 23f84f37
---
 pretyping/nativenorm.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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