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.

---
 parsing/g_vernac.ml4 | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 72c3cc14a1..7e7a887d30 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -165,16 +165,6 @@ GEXTEND Gram
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-	  let cum =
-	    match cum with
-	      Some true -> LocalCumulativity
-            | Some false -> LocalNonCumulativity
-	    | None ->
-                if Flags.is_polymorphic_inductive_cumulativity () then
-                  GlobalCumulativity
-                else
-                  GlobalNonCumulativity
-	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (NoDischarge, recs)
-- 
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

---
 parsing/g_vernac.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7e7a887d30..b947253b71 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -161,7 +161,7 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b)
       (* Gallina inductive declarations *)
-      | cum = cumulativity_token; priv = private_token; f = finite_token;
+      | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
           let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
@@ -247,7 +247,8 @@ GEXTEND Gram
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
   cumulativity_token:
-    [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ]
+    [ [ IDENT "Cumulative" -> VernacCumulative
+      | IDENT "NonCumulative" -> VernacNonCumulative ] ]
   ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
-- 
cgit v1.2.3