From e333c2fa6d97e79b389992412846adc71eb7abda Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 17:41:38 +0200
Subject: Improve errors for cumulativity when monomorphic

We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
---
 intf/vernacexpr.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 6ef9532ad7..2adf522b74 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -305,6 +305,14 @@ type inline =
 type module_ast_inl = module_ast * inline
 type module_binder = bool option * lident list * module_ast_inl
 
+(** Cumulativity can be set globally, locally or unset locally and it
+   can not enabled at all. *)
+type cumulative_inductive_parsing_flag =
+  | GlobalCumulativity
+  | GlobalNonCumulativity
+  | LocalCumulativity
+  | LocalNonCumulativity
+
 (** {6 The type of vernacular expressions} *)
 
 type vernac_expr =
@@ -336,7 +344,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-- 
cgit v1.2.3