diff options
| author | Amin Timany | 2017-07-28 17:41:38 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | e333c2fa6d97e79b389992412846adc71eb7abda (patch) | |
| tree | b3fc3e294820d72545f9647817e95eacf24422da /parsing | |
| parent | 3b7e7f7738737475cb0f09130b0487c85906dd2b (diff) | |
Improve errors for cumulativity when monomorphic
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
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 568818c270..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_polymorphic_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" -> |