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 *)
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 279b587831..8572870407 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -429,6 +429,7 @@ type vernac_expr =
       (Conv_oracle.level * reference or_by_notation list) list
   | VernacUnsetOption of Goptions.option_name
   | VernacSetOption of Goptions.option_name * option_value
+  | VernacSetAppendOption of Goptions.option_name * string
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
-- 
cgit v1.2.3


From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Oct 2016 13:27:29 +0200
Subject: Quick fix to #4595 (making notations containing "ltac:" unused for
 printing).

Also getting rid of a global side-effect.
---
 intf/notation_term.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 883b017727..1ab9980a5c 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -73,10 +73,11 @@ type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
+type reversibility_flag = bool
+
 type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
   ninterp_rec_vars : Id.t Id.Map.t;
-  mutable ninterp_only_parse : bool;
 }
 
 type grammar_constr_prod_item =
-- 
cgit v1.2.3