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 *) --- stm/vernac_classifier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/vernac_classifier.ml') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fa7acd00a..dc5be08a3 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 _ -- cgit v1.2.3