From c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.
---
 kernel/vmvalues.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/vmvalues.mli')

diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 350f71372..570e3606a 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -57,7 +57,7 @@ val cofix_upd_code : to_update -> tcode
 type atom =
   | Aid of Vars.id_key
   | Aind of inductive
-  | Atype of Univ.Universe.t
+  | Asort of Sorts.t
 
 (** Zippers *)
 
@@ -70,7 +70,6 @@ type zipper =
 type stack = zipper list
 
 type whd =
-  | Vsort of Sorts.t
   | Vprod of vprod
   | Vfun of vfun
   | Vfix of vfix * arguments option
-- 
cgit v1.2.3