aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-07-28 13:29:36 +0200
committerGravatar Amin Timany <amintimany@gmail.com>2017-07-31 18:05:54 +0200
commit3b7e7f7738737475cb0f09130b0487c85906dd2b (patch)
tree5e3990e47e793837f0ff2b6d7b87dba310ee535d /parsing
parent28998d55aaaf0ad0e78477db5601a5bc9a6657b1 (diff)
Change the option for cumulativity
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3d29fca77..568818c27 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -169,7 +169,7 @@ GEXTEND Gram
let cum =
match cum with
Some b -> b
- | None -> Flags.is_inductive_cumulativity ()
+ | None -> Flags.is_polymorphic_inductive_cumulativity ()
in
VernacInductive (cum, priv,f,indl)
| "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->