1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
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.
#[export] 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.
#[export] 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.
|
