diff options
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" -> |