blob: 5ce1ddf0c4b6f45cbc2fda4d99e03b6d6552c410 (
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
25
26
27
28
29
30
31
32
33
34
35
36
|
Module a.
Local Hint Extern 0 => progress subst.
Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
Proof.
intros.
(* this should not fail *)
progress eauto.
Defined.
End a.
Module b.
Local Hint Extern 0 => progress subst.
Goal forall T (x y : T) (P Q : _ -> Prop), y = x -> (P x -> Q x) -> P y -> Q y.
Proof.
intros.
eauto.
Defined.
End b.
Module c.
Local Hint Extern 0 => progress subst; eauto.
Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
Proof.
intros.
eauto.
Defined.
End c.
Module d.
Local Hint Extern 0 => progress subst; repeat match goal with H : _ |- _ => revert H end.
Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
Proof.
intros.
debug eauto.
Defined.
End d.
|
