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


From 4da21316ddc334f82ef830baca9e6d68cc73c59c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 5 Oct 2016 11:32:31 +0200
Subject: Fixing a beautifier bug pointed out by Emilio.

---
 printing/ppconstr.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index aa0ebbb83b..fa5a708995 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -370,13 +370,13 @@ end) = struct
     let n = begin_of_binders bl in
     match bl with
       | [LocalRawAssum (nal,k,t)] ->
-        pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
+        kw n ++ pr_binder false pr_c (nal,k,t)
       | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
-        pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
+        kw n ++ pr_undelimited_binders sep pr_c bdl
       | _ -> assert false
 
   let pr_binders_gen pr_c sep is_open =
-    if is_open then pr_delimited_binders mt sep pr_c
+    if is_open then pr_delimited_binders pr_com_at sep pr_c
     else pr_undelimited_binders sep pr_c
 
   let rec extract_prod_binders = function
@@ -525,9 +525,9 @@ end) = struct
     prlist_with_sep pr_semicolon
       (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
 
-  let pr_forall () = keyword "forall" ++ spc ()
+  let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
 
-  let pr_fun () = keyword "fun" ++ spc ()
+  let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
 
   let pr_fun_sep = spc () ++ str "=>"
 
-- 
cgit v1.2.3