From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Oct 2015 14:11:19 +0200
Subject: Goptions: new value type: optional string

These options can be set to a string value, but also unset.
Internal data is of type string option.
---
 printing/ppvernac.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 71dcd15cc7..76f97fce1e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -166,6 +166,8 @@ module Make
     (* This should not happen because of the grammar *)
       | IntValue (Some n) -> spc() ++ int n
       | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
       | BoolValue b -> mt()
     in pr_printoption a None ++ pr_opt_value b
 
-- 
cgit v1.2.3