From 250412bbacb2bf013d94b0b2458120e18c07c8fe Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Sep 2023 21:47:59 +0200
Subject: [PATCH] clarify efeed a bit and add some tests

---
 stdpp/tactics.v   |  2 +-
 tests/tactics.ref |  2 ++
 tests/tactics.v   | 21 +++++++++++++++++++++
 3 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index 65d7ab7a..cdb7488f 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -545,7 +545,7 @@ Tactic Notation "efeed_core" constr(H) "using" tactic3(tac) :=
   | ?T1 → ?T2 =>
     let HT1 := fresh "feed" in assert T1 as HT1;
       [| go (H HT1); clear HT1 ]
-  | ?T1 → _ =>
+  | ∀ x : ?T1, _ =>
     let e := mk_evar T1 in
     go (H e)
   | ?T1 => tac H
diff --git a/tests/tactics.ref b/tests/tactics.ref
index be6d2967..21ef6edc 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -4,3 +4,5 @@ The command has indeed failed with message:
 Failed to progress.
 The command has indeed failed with message:
 Failed to progress.
+The command has indeed failed with message:
+Failed to progress.
diff --git a/tests/tactics.v b/tests/tactics.v
index 8272a640..bb2e4680 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -116,3 +116,24 @@ Proof.
   let f' := get_head (f 0 1 2) in unify f f'.
   let f' := get_head f in unify f f'.
 Abort.
+
+(** (e)feed tests *)
+Lemma feed1 (P Q R : Prop) :
+  P → Q → (P → Q → R) → R.
+Proof.
+  intros HP HQ HR.
+  feed specialize HR; [exact HP|exact HQ|exact HR].
+Restart.
+  intros HP HQ HR.
+  feed pose proof HR as HR'; [exact HP|exact HQ|exact HR'].
+Qed.
+Lemma efeed1 (P Q R : nat → Prop) :
+  P 1 → Q 1 → (∀ n, P n → Q n → R n) → R 1.
+Proof.
+  intros HP HQ HR.
+  Fail progress feed specialize HR.
+  efeed specialize HR; [exact HP|exact HQ|exact HR].
+Restart.
+  intros HP HQ HR.
+  efeed pose proof HR as HR'; [exact HP|exact HQ|exact HR'].
+Qed.
-- 
GitLab