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 /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions