From f4de78b048f6567f1e1fdd553b4f7ada0e0707b8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 20:45:05 +0200
Subject: Do not add "Append" as a lexer keyword.

This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
---
 parsing/g_vernac.ml4 | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 96eede2b96..bc02a46218 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -850,9 +850,15 @@ GEXTEND Gram
 
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_value ->
-  	  VernacSetOption (table,v)
-      | "Set"; table = option_table; "Append"; v = STRING ->
-         VernacSetAppendOption (table,v)
+        begin match v with
+        | StringValue s ->
+          let (last, prefix) = List.sep_last table in
+          if String.equal last "Append" && not (List.is_empty prefix) then
+            VernacSetAppendOption (prefix, s)
+          else
+            VernacSetOption (table, v)
+        | _ -> VernacSetOption (table, v)
+        end
       | "Set"; table = option_table ->
   	  VernacSetOption (table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
-- 
cgit v1.2.3