From 9c5a447688365006c8e594edfb1e973db8d53454 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 19 Mar 2018 14:13:01 +0100
Subject: Make parsing independent of the cumulativity flag.

---
 printing/ppvernac.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5c5b7206a5..b7f5a8309d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -788,8 +788,9 @@ open Decl_kinds
           if p then
             let cm =
               match cum with
-              | GlobalCumulativity | LocalCumulativity -> "Cumulative"
-              | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative"
+              | Some true -> "Cumulative"
+              | Some false -> "NonCumulative"
+              | None -> ""
             in
             cm ^ " " ^ kind
           else kind
-- 
cgit v1.2.3


From bca95952b541b209a3f8ca44d1ff119b976e54fb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 22 Mar 2018 13:21:41 +0100
Subject: bool option -> (VernacCumulative | VernacNonCumulative) option

---
 printing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b7f5a8309d..8180e45034 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -788,8 +788,8 @@ open Decl_kinds
           if p then
             let cm =
               match cum with
-              | Some true -> "Cumulative"
-              | Some false -> "NonCumulative"
+              | Some VernacCumulative -> "Cumulative"
+              | Some VernacNonCumulative -> "NonCumulative"
               | None -> ""
             in
             cm ^ " " ^ kind
-- 
cgit v1.2.3