diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /vernac/himsg.ml | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
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.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 *) |