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/environ.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index ab046f02f7..5f6d5f3d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,7 +59,8 @@ type globals = {
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement
+  env_engagement : engagement;
+  env_sprop_allowed : bool;
 }
 
 type val_kind =
@@ -117,7 +118,9 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet };
+    env_engagement = PredicativeSet;
+    env_sprop_allowed = false;
+  };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab }
@@ -243,7 +246,7 @@ let is_impredicative_set env =
   | _ -> false
 
 let is_impredicative_sort env = function
-  | Sorts.Prop -> true
+  | Sorts.SProp | Sorts.Prop -> true
   | Sorts.Set -> is_impredicative_set env
   | Sorts.Type _ -> false
 
@@ -432,6 +435,14 @@ let set_typing_flags c env = (* Unsafe *)
   if same_flags env.env_typing_flags c then env
   else { env with env_typing_flags = c }
 
+let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative
+
+let set_allow_sprop b env =
+  { env with env_stratification =
+    { env.env_stratification with env_sprop_allowed = b } }
+
+let sprop_allowed env = env.env_stratification.env_sprop_allowed
+
 (* Global constants *)
 
 let no_link_info = NotLinked
-- 
cgit v1.2.3


From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 kernel/environ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5f6d5f3d0e..97c9f8654a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -548,7 +548,7 @@ let lookup_projection p env =
   match mib.mind_record with
   | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection")
   | PrimRecord infos ->
-    let _,_,typs = infos.(i) in
+    let _,_,_,typs = infos.(i) in
     typs.(Projection.arg p)
 
 let get_projection env ind ~proj_arg =
-- 
cgit v1.2.3