From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

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

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b605a44c87..e6b28b1d87 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -162,11 +162,16 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((Some Discharge, Definition), (id, None), b)
       (* Gallina inductive declarations *)
-      | priv = private_token; f = finite_token;
+      | cum = 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
-          VernacInductive (priv,f,indl)
+          let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
+	  let cum =
+	    match cum with
+	      Some b -> b
+	    | None -> Flags.is_inductive_cumulativity ()
+	  in
+          VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -234,6 +239,9 @@ GEXTEND Gram
       | IDENT "Structure" -> (Structure,BiFinite)
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
+  cumulativity_token:
+    [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ]
+  ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;
-- 
cgit v1.2.3