From 805211a603431f4ba351e0164b0bd147a771a1a0 Mon Sep 17 00:00:00 2001
From: Dabrowski
Date: Wed, 5 Jun 2019 00:00:18 +0200
Subject: allow empty tactic_rules in ARGUMENT EXTEND

---
 coqpp/coqpp_parse.mly     |  2 +-
 plugins/ssr/ssrparser.mlg | 10 +---------
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 43ba990f6a..f7959f8201 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -270,7 +270,7 @@ tactic_level:
 ;
 
 tactic_rules:
-| tactic_rule { [$1] }
+| { [] }
 | tactic_rule tactic_rules { $1 :: $2 }
 ;
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 27a558611e..ba23d149ce 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -79,7 +79,6 @@ let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
 }
 
 ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
-| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
 END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrtacarg;
@@ -88,7 +87,6 @@ END
 
 (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
 ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
-| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
 END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrtac3arg;
@@ -1005,7 +1003,6 @@ let pr_ssrfwdidx _ _ _ = pr_ssrfwdid
 (* We use a primitive parser for the head identifier of forward *)
 (* tactis to avoid syntactic conflicts with basic Coq tactics. *)
 ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx }
-  | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 {
@@ -1564,7 +1561,6 @@ let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) =
 ARGUMENT EXTEND ssrdoarg
   TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses)
   PRINTED BY { pr_ssrdoarg env sigma }
-| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 {
@@ -1587,7 +1583,7 @@ let pr_ssrseqarg env sigma _ _ prt = function
 (* an unindexed tactic.                                            *)
 ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option))
                           PRINTED BY { pr_ssrseqarg env sigma }
-| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
+
 END
 
 {
@@ -1867,7 +1863,6 @@ let pr_ssrseqdir _ _ _ = function
 }
 
 ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir }
-| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 TACTIC EXTEND ssrtclseq
@@ -2004,7 +1999,6 @@ let pr_ssreqid _ _ _ = pr_eqid
 (* We must use primitive parsing here to avoid conflicts with the  *)
 (* basic move, case, and elim tactics.                             *)
 ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY { pr_ssreqid }
-| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 {
@@ -2326,7 +2320,6 @@ let noruleterm loc = mk_term xNoFlag (mkCProp loc)
 }
 
 ARGUMENT EXTEND ssrrule_ne TYPED AS (ssrrwkind * ssrterm) PRINTED BY { pr_ssrrule }
-  | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 GRAMMAR EXTEND Gram
@@ -2413,7 +2406,6 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs
 }
 
 ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs }
-  | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
 {
-- 
cgit v1.2.3