From 9c5a447688365006c8e594edfb1e973db8d53454 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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 72c3cc14a..7e7a887d3 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