From b3dbd589e1dc41d7bce18afd87dd6e59968286bb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 30 Sep 2016 22:50:49 +0200
Subject: Add command 'Set foo Append "bar"' for appending to an option (bug
 #5109).

For now, the only meaningful user is "Set Warnings". Example:

Section Bar.
  Local Set Warnings Append "-foo".
  (* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
---
 printing/ppvernac.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2d87b51d73..f4a112a4cb 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1110,6 +1110,11 @@ module Make
         return (
           hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
         )
+      | VernacSetAppendOption (na,v) ->
+        return (
+          hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
+                   spc() ++ keyword "Append" ++ spc() ++ str v)
+        )
       | VernacAddOption (na,l) ->
         return (
           hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
-- 
cgit v1.2.3