aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4762.v
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-09-28 10:40:54 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-30 09:10:06 +0200
commit844b076bf5150a107d31cd4648955c3a6538a34b (patch)
tree465b7a102e879a267b0a0c24b4db59f17a8b84e0 /test-suite/bugs/closed/4762.v
parent4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 (diff)
Fix #4762.
Diffstat (limited to 'test-suite/bugs/closed/4762.v')
-rw-r--r--test-suite/bugs/closed/4762.v24
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v
new file mode 100644
index 000000000..7a87b07a8
--- /dev/null
+++ b/test-suite/bugs/closed/4762.v
@@ -0,0 +1,24 @@
+Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q.
+
+Lemma foo P Q R : R = myand P Q -> P -> Q -> R.
+Proof. intros ->; constructor; auto. Qed.
+
+Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+ intros.
+ eauto with test1.
+Qed.
+
+Hint Extern 0 =>
+ match goal with
+ | |- myand _ _ => eapply foo; [reflexivity| |]
+ end : test2.
+
+Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R).
+Proof.
+ intros.
+ eauto with test2. (* works *)
+Qed.
+