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 /printing/ppvernac.ml | |
| 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 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a68b569cbe..4c50c2f368 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -760,7 +760,11 @@ open Decl_kinds | Class _ -> "Class" | Variant -> "Variant" in if p then - let cm = if cum then "Cumulative" else "NonCumulative" in + let cm = + match cum with + | GlobalCumulativity | LocalCumulativity -> "Cumulative" + | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + in cm ^ " " ^ kind else kind in |