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.
---
 API/API.mli | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 19726b52f2..d39d3cb25c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3780,6 +3780,12 @@ sig
     | DefaultInline
     | InlineAt of int
 
+  type cumulative_inductive_parsing_flag =
+    | GlobalCumulativity
+    | GlobalNonCumulativity
+    | LocalCumulativity
+    | LocalNonCumulativity
+
   type vernac_expr =
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_expr Loc.located
@@ -3804,7 +3810,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-- 
cgit v1.2.3