From 39514550177a887a526a66b8ec080cae5c463a9d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Apr 2011 07:11:39 +0000
Subject: Fixing an "apply -> ... in hyp" bug (the hyp was considered as a
 fixed ident by Ltac).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14074 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/apply.v | 7 +++++++
 theories/Init/Tactics.v    | 4 ++--
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index d1efbca85a..32d82bd1a8 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -202,6 +202,13 @@ try apply H.
 unfold ID; apply H0.
 Qed.
 
+(* Test hyp in "apply -> ... in hyp" is correctly instantiated by Ltac *)
+
+Goal (True <-> False) -> True -> False.
+intros Heq H.
+match goal with [ H : True |- _ ] => apply -> Heq in H end.
+Abort.
+
 (* Test coercion below product and on non meta-free terms in with bindings *)
 (* Cf wishes #1408 from E. Makarov *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 82951f92dc..2caf6a4b8d 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -153,10 +153,10 @@ bapply lemma ltac:(fun H => destruct H as [H _]; apply H).
 Tactic Notation "apply" "<-" constr(lemma) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).
 
-Tactic Notation "apply" "->" constr(lemma) "in" ident(J) :=
+Tactic Notation "apply" "->" constr(lemma) "in" hyp(J) :=
 bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
 
-Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
+Tactic Notation "apply" "<-" constr(lemma) "in" hyp(J) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
 
 (** An experimental tactic simpler than auto that is useful for ending
-- 
cgit v1.2.3