From bca95952b541b209a3f8ca44d1ff119b976e54fb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 22 Mar 2018 13:21:41 +0100 Subject: bool option -> (VernacCumulative | VernacNonCumulative) option --- parsing/g_vernac.ml4 | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'parsing') 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 ] ] -- cgit v1.2.3