blob: 43eb1377d2c4eb07aa89970ddb51d18195ecaef4 (
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
37
|
Module a.
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 *)
Fail progress eauto.
admit.
Defined.
End a.
Module b.
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.
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.
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.
eauto.
Defined.
End d.
|