Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 6 insertions, 2 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index dc6607557d..35a7036af4 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,6 +60,7 @@ type pretype_error =
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
     (Evar.t * Evar_kinds.t) option * Evar.Set.t option
+  | DisallowedSProp
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -107,9 +108,9 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys =
   raise_type_error ?loc
     (env, sigma, IllTypedRecBody (i, na, jl, tys))
 
-let error_elim_arity ?loc env sigma pi s c j a =
+let error_elim_arity ?loc env sigma pi c j a =
   raise_type_error ?loc
-    (env, sigma, ElimArity (pi, s, c, j, a))
+    (env, sigma, ElimArity (pi, c, j, a))
 
 let error_not_a_type ?loc env sigma j =
   raise_type_error ?loc (env, sigma, NotAType j)
@@ -171,6 +172,9 @@ let error_var_not_found ?loc env sigma s =
 let error_evar_not_found ?loc env sigma id =
   raise_pretype_error ?loc (env, sigma, EvarNotFound id)
 
+let error_disallowed_sprop env sigma  =
+  raise (PretypeError (env, sigma, DisallowedSProp))
+
 (*s Typeclass errors *)
 
 let unsatisfiable_constraints env evd ev comp =