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/term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 58b289eaa5..d791fe67e5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -19,7 +19,7 @@ open Constr
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
-type sorts = Sorts.t =
+type sorts = Sorts.t = private
   | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.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/term.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index d791fe67e5..e67c2130d5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -16,11 +16,11 @@ open Vars
 open Constr
 
 (* Deprecated *)
-type sorts_family = Sorts.family = InProp | InSet | InType
+type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
 type sorts = Sorts.t = private
-  | Prop | Set
+  | SProp | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
 
-- 
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/term.ml | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index e67c2130d5..f09c45715f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -14,6 +14,7 @@ open CErrors
 open Names
 open Vars
 open Constr
+open Context
 
 (* Deprecated *)
 type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
@@ -32,9 +33,11 @@ type sorts = Sorts.t = private
 (* Other term constructors *)
 (***************************)
 
-let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c)
-let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
-let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2)
+let name_annot = map_annot Name.mk_name
+
+let mkNamedProd id typ c = mkProd (name_annot id, typ, subst_var id.binder_name c)
+let mkNamedLambda id typ c = mkLambda (name_annot id, typ, subst_var id.binder_name c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (name_annot id, c1, t, subst_var id.binder_name c2)
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
 let mkProd_or_LetIn decl c =
@@ -60,10 +63,11 @@ let mkNamedProd_wo_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
     | LocalAssum (id,t) -> mkNamedProd id t c
-    | LocalDef (id,b,_t) -> subst1 b (subst_var id c)
+    | LocalDef (id,b,_) -> subst1 b (subst_var id.binder_name c)
 
 (* non-dependent product t1 -> t2 *)
-let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
+let mkArrow t1 r t2 = mkProd (make_annot Anonymous r, t1, t2)
+let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
 
 (* Constructs either [[x:t]c] or [[x=b:t]c] *)
 let mkLambda_or_LetIn decl c =
@@ -366,8 +370,8 @@ let rec isArity c =
 type ('constr, 'types) kind_of_type =
   | SortType   of Sorts.t
   | CastType   of 'types * 'types
-  | ProdType   of Name.t * 'types * 'types
-  | LetInType  of Name.t * 'constr * 'types * 'types
+  | ProdType   of Name.t Context.binder_annot * 'types * 'types
+  | LetInType  of Name.t Context.binder_annot * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
 
 let kind_of_type t = match kind t with
-- 
cgit v1.2.3