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(-)

(limited to 'parsing')

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


From 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Oct 2016 00:10:55 +0200
Subject: Fix bug #5098: Symmetry broken in HoTT.

We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
---
 parsing/g_tactic.ml4 | 2 +-
 parsing/pcoq.ml      | 1 +
 parsing/pcoq.mli     | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 199ef9fcee..3152afb28d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -220,7 +220,7 @@ let warn_deprecated_eqn_syntax =
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl hypident destruction_arg;
+  simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 4e069c9e33..9e9a7e723e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -350,6 +350,7 @@ module Tactic =
     let red_expr = make_gen_entry utactic "red_expr"
     let simple_intropattern =
       make_gen_entry utactic "simple_intropattern"
+    let in_clause = make_gen_entry utactic "in_clause"
     let clause_dft_concl = 
       make_gen_entry utactic "clause"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7f49c997fe..7f6caf63fb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -193,6 +193,7 @@ module Tactic :
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_tactic_expr Gram.entry
     val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+    val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
-- 
cgit v1.2.3