From d1ed4016b30e9989a56a70968526f27c3be694eb Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 26 Feb 2020 00:47:56 +0100
Subject: [PATCH] Generalize (e)feed pose proof to intro patterns

This appears a simple oversight, since `pose proof` takes an intro pattern
anyway; `feed inversion` and `feed destruct` already take intro patterns, and
I've been using the generalized `efeed pose proof` for a while.
---
 theories/tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 4045a47e..d715c743 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -427,12 +427,12 @@ Tactic Notation "efeed" constr(H) "using" tactic3(tac) :=
 
 (** The following variants of [pose proof], [specialize], [inversion], and
 [destruct], use the [feed] tactic before invoking the actual tactic. *)
-Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+Tactic Notation "feed" "pose" "proof" constr(H) "as" simple_intropattern(H') :=
   feed (fun p => pose proof p as H') H.
 Tactic Notation "feed" "pose" "proof" constr(H) :=
   feed (fun p => pose proof p) H.
 
-Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+Tactic Notation "efeed" "pose" "proof" constr(H) "as" simple_intropattern(H') :=
   efeed H using (fun p => pose proof p as H').
 Tactic Notation "efeed" "pose" "proof" constr(H) :=
   efeed H using (fun p => pose proof p).
-- 
GitLab