Merge PR #9027: Refactor checking of inductive types

Ack-by: SkySkimmer
Reviewed-by: mattam82
Ack-by: maximedenes
Ack-by: ppedrot

4 files changed, 7 insertions, 6 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 25a4804743..92b1ff7572 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -24,7 +24,7 @@ open Constrexpr_ops
 open Constrintern
 open Impargs
 open Reductionops
-open Indtypes
+open Type_errors
 open Pretyping
 open Indschemes
 open Context.Rel.Declaration
@@ -304,7 +304,7 @@ let inductive_levels env evd poly arities inds =
         let evd =
           if Sorts.is_set du then
             if not (Evd.check_leq evd cu Univ.type0_univ) then
-              raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
+              raise (InductiveError LargeNonPropInductiveNotInType)
             else evd
           else evd
             (* Evd.set_leq_sort env evd (Type cu) du *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index e1496e58d7..71770a21ca 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open CErrors
-open Indtypes
 open Type_errors
 open Pretype_errors
 open Indrec
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f3e1e1fc49..ebbec86b9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -15,7 +15,6 @@ open Nameops
 open Namegen
 open Constr
 open Termops
-open Indtypes
 open Environ
 open Pretype_errors
 open Type_errors
@@ -1163,6 +1162,9 @@ let error_bad_entry () =
 let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
+let error_inductive_bad_univs () =
+  str "Incorrect universe constrains declared for inductive type."
+
 (* Recursion schemes errors *)
 
 let error_not_allowed_case_analysis env isrec kind i =
@@ -1199,7 +1201,8 @@ let explain_inductive_error = function
   | NotAnArity (env, c) -> error_not_an_arity env c
   | BadEntry -> error_bad_entry ()
   | LargeNonPropInductiveNotInType ->
-      error_large_non_prop_inductive_not_in_type ()
+    error_large_non_prop_inductive_not_in_type ()
+  | BadUnivs -> error_inductive_bad_univs ()
 
 (* Recursion schemes errors *)
 
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index bab66b2af4..986906d303 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Indtypes
 open Environ
 open Type_errors
 open Pretype_errors