diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-19 14:13:01 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-21 15:51:42 +0100 |
| commit | 9c5a447688365006c8e594edfb1e973db8d53454 (patch) | |
| tree | 780e5bd2163f4af68c5d1e2144e432637301b838 /parsing | |
| parent | f21deb6c861b359f0d3bf8b170d277cfa0d80171 (diff) | |
Make parsing independent of the cumulativity flag.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 0 insertions, 10 deletions
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) |