diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 10:04:07 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-04-05 10:04:07 +0200 |
| commit | 4c3564ac7e2ea231a6dde84f2af6bfddbc0834c6 (patch) | |
| tree | ba0f9bbbc04048c48a2128dde5bb89b2517e52c8 /parsing | |
| parent | f97498a6c104da9b7b31f84505db76194a566f9b (diff) | |
| parent | bca95952b541b209a3f8ca44d1ff119b976e54fb (diff) | |
Merge PR #7016: Make parsing independent of the cumulativity flag.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8b445985b..593dcbf58 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -161,20 +161,10 @@ 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 - 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) @@ -257,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 ] ] |