diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-22 13:21:41 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-22 13:21:41 +0100 |
| commit | bca95952b541b209a3f8ca44d1ff119b976e54fb (patch) | |
| tree | cc4f6d8a466a0862a8fa3b4c0db8beef4a4c43c8 /parsing | |
| parent | 9c5a447688365006c8e594edfb1e973db8d53454 (diff) | |
bool option -> (VernacCumulative | VernacNonCumulative) option
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7e7a887d3..b947253b7 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 ] ] |