From 9c5a447688365006c8e594edfb1e973db8d53454 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Mar 2018 14:13:01 +0100
Subject: Make parsing independent of the cumulativity flag.

---
 vernac/vernacentries.ml | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3dbe8b0c09..479f9725ec 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl =
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let should_treat_as_cumulative cum poly =
-  if poly then
-    match cum with
-    | GlobalCumulativity | LocalCumulativity -> true
-    | GlobalNonCumulativity | LocalNonCumulativity -> false
-  else
-    match cum with
-    | GlobalCumulativity | GlobalNonCumulativity -> false
-    | LocalCumulativity -> 
-      user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
-    | LocalNonCumulativity ->
-      user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+  match cum with
+  | Some true ->
+    if poly then true
+    else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
+  | Some false ->
+    if poly then false
+    else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
+  | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
 
 let vernac_record cum k poly finite struc binders sort nameopt cfs =
   let is_cumulative = should_treat_as_cumulative cum poly in
-- 
cgit v1.2.3


From bca95952b541b209a3f8ca44d1ff119b976e54fb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 22 Mar 2018 13:21:41 +0100
Subject: bool option -> (VernacCumulative | VernacNonCumulative) option

---
 vernac/vernacentries.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 479f9725ec..1f6f9fa982 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -535,10 +535,10 @@ let vernac_assumption ~atts discharge kind l nl =
 
 let should_treat_as_cumulative cum poly =
   match cum with
-  | Some true ->
+  | Some VernacCumulative ->
     if poly then true
     else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
-  | Some false ->
+  | Some VernacNonCumulative ->
     if poly then false
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
@@ -562,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs =
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
-  let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -599,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
+    let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
     ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
 
 let vernac_fixpoint ~atts discharge l =
-- 
cgit v1.2.3