From bca95952b541b209a3f8ca44d1ff119b976e54fb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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 b7f5a8309..8180e4503 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