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 *)

1 files changed, 5 insertions, 0 deletions

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))