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

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index d3f346d76b..205a3984d5 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -146,6 +146,7 @@ let make_senv () =
   let senv = Safe_typing.set_engagement !impredicative_set senv in
   let senv = Safe_typing.set_indices_matter !indices_matter senv in
   let senv = Safe_typing.set_VM false senv in
+  let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
   Safe_typing.set_native_compiler false senv
 
 let admit_list = ref ([] : object_file list)
@@ -296,6 +297,7 @@ let explain_exn = function
       | IllFormedRecBody _ -> str"IllFormedRecBody"
       | IllTypedRecBody _ -> str"IllTypedRecBody"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
+      | DisallowedSProp -> str"DisallowedSProp"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
   | InductiveError e ->
-- 
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.
---
 checker/checker.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index 205a3984d5..9be88ee31e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -298,6 +298,7 @@ let explain_exn = function
       | IllTypedRecBody _ -> str"IllTypedRecBody"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
+      | BadRelevance -> str"BadRelevance"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
   | InductiveError e ->
-- 
cgit v1.2.3


From 06b29ed748a9d9b99c2c08a3788906dbad5417d2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Jun 2018 13:57:28 +0200
Subject: Repair relevance marks in-kernel.

Prevent errors when under annotating binders.
---
 checker/checker.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'checker/checker.ml')

diff --git a/checker/checker.ml b/checker/checker.ml
index 9be88ee31e..cbac9cb570 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -386,6 +386,7 @@ let init_with_argv argv =
   let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
   try
     parse_args argv;
+    CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name);
     if !Flags.debug then Printexc.record_backtrace true;
     Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
     Flags.if_verbose print_header ();
-- 
cgit v1.2.3