From 6eb05dfc40feef58063bb537fb742eb16bbf86d1 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 6 May 2020 21:18:06 +0200
Subject: [PATCH] tactics.v: Fix parsing precedence for `select` tactic

---
 theories/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 5fd8ee7e..e3cb1f96 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -531,7 +531,7 @@ matching hypotheses.
 [select] is written in CPS and does not return the name of the
 hypothesis due to limitations in the Ltac1 tactic runtime (see
 https://gitter.im/coq/coq?at=5e96c82f85b01628f04bbb89). *)
-Tactic Notation "select" open_constr(pat) tactic(tac) :=
+Tactic Notation "select" open_constr(pat) tactic3(tac) :=
   lazymatch goal with
   (* The [unify] is necessary, otherwise holes in [pat] stay as side-conditions *)
   | H : pat |- _ => let T := (type of H) in unify T pat; tac H
-- 
GitLab