From e333c2fa6d97e79b389992412846adc71eb7abda Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Jul 2017 17:41:38 +0200
Subject: 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.
---
 printing/ppvernac.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'printing')

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
-- 
cgit v1.2.3