From c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 25 Feb 2018 16:28:00 +0100
Subject: [VM] Unify Const_sorts and Const_type, and remove Vsort.

This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
---
 pretyping/vnorm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c93b41786b..6b7ea2996d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -141,7 +141,6 @@ and nf_vtype env sigma v =  nf_val env sigma v crazy_type
 
 and nf_whd env sigma whd typ =
   match whd with
-  | Vsort s -> mkSort s
   | Vprod p ->
       let dom = nf_vtype env sigma (dom p) in
       let name = Name (Id.of_string "x") in
@@ -182,7 +181,8 @@ and nf_whd env sigma whd typ =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
      in
      nf_univ_args ~nb_univs mk env sigma stk
-  | Vatom_stk(Atype u, stk) -> assert false
+  | Vatom_stk(Asort s, stk) ->
+    assert (List.is_empty stk); mkSort s
   | Vuniv_level lvl ->
     assert false
 
-- 
cgit v1.2.3