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.
---
 vernac/himsg.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'vernac/himsg.ml')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2ef2317d86..fd5970e8ca 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -710,6 +710,9 @@ let explain_undeclared_universe env sigma l =
     Termops.pr_evd_level sigma l ++
     spc () ++ str "(maybe a bugged tactic)."
 
+let explain_disallowed_sprop () =
+  Pp.(str "SProp not allowed, you need to use -allow-sprop.")
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -751,6 +754,7 @@ let explain_type_error env sigma err =
       explain_unsatisfied_constraints env sigma cst
   | UndeclaredUniverse l ->
      explain_undeclared_universe env sigma l
+  | DisallowedSProp -> explain_disallowed_sprop ()
 
 let pr_position (cl,pos) =
   let clpos = match cl with
@@ -864,6 +868,7 @@ let explain_pretype_error env sigma err =
   | TypingError t -> explain_type_error env sigma t
   | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e
   | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
+  | DisallowedSProp -> explain_disallowed_sprop ()
 
 (* Module errors *)
 
-- 
cgit v1.2.3