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/sorts.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/sorts.mli')

diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 6c5ce4df80..3ca76645db 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,7 +12,7 @@
 
 type family = InProp | InSet | InType
 
-type t =
+type t = private
   | Prop
   | Set
   | Type of Univ.Universe.t
@@ -42,6 +42,8 @@ end
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
 
+val super : t -> t
+
 val debug_print : t -> Pp.t
 
 val pr_sort_family : family -> Pp.t
-- 
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/sorts.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/sorts.mli')

diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 3ca76645db..65078c2a62 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -10,13 +10,15 @@
 
 (** {6 The sorts of CCI. } *)
 
-type family = InProp | InSet | InType
+type family = InSProp | InProp | InSet | InType
 
 type t = private
+  | SProp
   | Prop
   | Set
   | Type of Univ.Universe.t
 
+val sprop : t
 val set  : t
 val prop : t
 val type1  : t
@@ -25,6 +27,7 @@ val equal : t -> t -> bool
 val compare : t -> t -> int
 val hash : t -> int
 
+val is_sprop : t -> bool
 val is_set : t -> bool
 val is_prop : t -> bool
 val is_small : t -> bool
@@ -32,6 +35,7 @@ val family : t -> family
 
 val hcons : t -> t
 
+val family_compare : family -> family -> int
 val family_equal : family -> family -> bool
 
 module List : sig
-- 
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/sorts.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'kernel/sorts.mli')

diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 65078c2a62..c49728b146 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -48,6 +48,16 @@ val sort_of_univ : Univ.Universe.t -> t
 
 val super : t -> t
 
+(** On binders: is this variable proof relevant *)
+type relevance = Relevant | Irrelevant
+
+val relevance_hash : relevance -> int
+
+val relevance_equal : relevance -> relevance -> bool
+
+val relevance_of_sort : t -> relevance
+val relevance_of_sort_family : family -> relevance
+
 val debug_print : t -> Pp.t
 
 val pr_sort_family : family -> Pp.t
-- 
cgit v1.2.3