aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:34:15 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:34:15 +0200
commitf0b4757d291ce3e07c8ccfcd4217d204fd2059ba (patch)
tree3a2a3db40ab962e91366fca5223b6f25c390a276 /parsing
parent83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff)
parent2f0e71c7e25eb193f252b6848dadff771dbc270d (diff)
Merge PR #864: Some cleanups after cumulativity for inductive types
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml49
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" ->