diff options
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 3d29fca779..93a778274d 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" -> |