Infrastructure for cumulative inductive syntax (no grammar extension yet)

1 files changed, 4 insertions, 0 deletions

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index bef9e29ac2..c4f7e77714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -744,6 +744,9 @@ let explain_bad_relevance env =
 let explain_bad_invert env =
   strbrk "Bad case inversion (maybe a bugged tactic)."
 
+let explain_bad_variance env sigma u =
+  str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma u ++ str"."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -788,6 +791,7 @@ let explain_type_error env sigma err =
   | DisallowedSProp -> explain_disallowed_sprop ()
   | BadRelevance -> explain_bad_relevance env
   | BadInvert -> explain_bad_invert env
+  | BadVariance u -> explain_bad_variance env sigma u
 
 let pr_position (cl,pos) =
   let clpos = match cl with