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/vernacexpr.mli') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 279b58783..857287040 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