From a0e16c9e5c3f88a8b72935dd4877f13388640f69 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 12 Oct 2017 13:55:08 +0200
Subject: Make Sorts.t private

---
 kernel/vmvalues.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9a3eadf747..ac5350e9fa 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 open Names
-open Sorts
 open Univ
 open Constr
 
@@ -335,10 +334,10 @@ let rec whd_accu a stk =
         let args = Array.init (nargs args) (arg args) in
         let s = Obj.obj (Obj.field at 0) in
         begin match s with
-        | Type u ->
+        | Sorts.Type u ->
           let inst = Instance.of_array (Array.map uni_lvl_val args) in
           let u = Univ.subst_instance_universe inst u in
-          Vatom_stk (Asort (Type u), [])
+          Vatom_stk (Asort (Sorts.sort_of_univ u), [])
         | _ -> assert false
         end
      | _ -> assert false
-- 
cgit v1.2.3


From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Oct 2017 14:03:51 +0200
Subject: Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
---
 kernel/vmvalues.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index ac5350e9fa..777a207013 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -137,6 +137,7 @@ let hash_annot_switch asw =
 let pp_sort s =
   let open Sorts in
   match s with
+  | SProp -> Pp.str "SProp"
   | Prop -> Pp.str "Prop"
   | Set -> Pp.str "Set"
   | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}")
-- 
cgit v1.2.3