From 9c678306157b2c6199091709ef7bb067f724f80c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Nov 2018 18:18:26 +0100
Subject: Refactor typechecking of inductive types

We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
---
 vernac/himsg.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 98c8c21699..ebbec86b9c 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1162,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 =
@@ -1198,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 *)
 
-- 
cgit v1.2.3