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/cbytegen.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cbytegen.ml')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 718584b3d4..af14baaca6 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -562,10 +562,10 @@ let rec compile_lam env cenv lam sz cont =
       compile_fv_elem cenv (FVuniv_var idx) sz cont
     in
     if List.is_empty s then
-      compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont
+      compile_structured_constant cenv (Const_sort (Sorts.sort_of_univ u)) sz cont
     else
       comp_app compile_structured_constant compile_get_univ cenv
-        (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
+        (Const_sort (Sorts.sort_of_univ u)) (Array.of_list s) sz cont
 
   | Llet (_id,def,body) ->
       compile_lam env cenv def sz
-- 
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/cbytegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cbytegen.ml')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index af14baaca6..69f004307d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -550,7 +550,7 @@ let rec compile_lam env cenv lam sz cont =
     else comp_app compile_structured_constant compile_universe cenv
         (Const_ind ind) (Univ.Instance.to_array u) sz cont
 
-  | Lsort (Sorts.Prop | Sorts.Set as s) ->
+  | Lsort (Sorts.SProp | Sorts.Prop | Sorts.Set as s) ->
     compile_structured_constant cenv (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
     (* We represent universes as a global constant with local universes
-- 
cgit v1.2.3