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, 1 insertions, 1 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fa7acd00ab..dc5be08a37 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -181,7 +181,7 @@ let rec classify_vernac e =
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacUnsetOption _ | VernacSetOption _
+    | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
     | VernacAddOption _ | VernacRemoveOption _
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _