aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4762.v
blob: 7a87b07a8ee60b2a68a6d9023c2d2d002848c8b2 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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.