diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:34:15 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:34:15 +0200 |
| commit | f0b4757d291ce3e07c8ccfcd4217d204fd2059ba (patch) | |
| tree | 3a2a3db40ab962e91366fca5223b6f25c390a276 /parsing | |
| parent | 83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff) | |
| parent | 2f0e71c7e25eb193f252b6848dadff771dbc270d (diff) | |
Merge PR #864: Some cleanups after cumulativity for inductive types
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3d29fca77..93a778274 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -168,8 +168,13 @@ GEXTEND Gram 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 () + 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" -> |