diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-27 20:16:35 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:16 +0200 |
| commit | 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac (patch) | |
| tree | 916f61f35650966d7a288e8579279b0a3e45afc6 /parsing | |
| parent | 7b5fcef8a0fb3b97a3980f10596137234061990f (diff) | |
Fix bugs and add an option for cumulativity
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b605a44c8..e6b28b1d8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -162,11 +162,16 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) - | priv = private_token; f = finite_token; + | cum = 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 - VernacInductive (priv,f,indl) + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in + let cum = + match cum with + Some b -> b + | None -> Flags.is_inductive_cumulativity () + in + VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -234,6 +239,9 @@ GEXTEND Gram | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; + cumulativity_token: + [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; |