diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-07-28 13:29:36 +0200 |
|---|---|---|
| committer | Amin Timany <amintimany@gmail.com> | 2017-07-31 18:05:54 +0200 |
| commit | 3b7e7f7738737475cb0f09130b0487c85906dd2b (patch) | |
| tree | 5e3990e47e793837f0ff2b6d7b87dba310ee535d /parsing | |
| parent | 28998d55aaaf0ad0e78477db5601a5bc9a6657b1 (diff) | |
Change the option for cumulativity
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
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" -> |