blob: 03034cf1305e8197a75e3030d6a77e5ddfef38b8 (
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
|
Goal forall x:nat, (forall x, x=0 -> True)->True.
intros; eapply H.
instantiate (1:=(fun y => _) (S x)).
simpl.
clear x. trivial.
Qed.
Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
intros; eapply H.
rename z into z'.
clear H0.
clear z'.
reflexivity.
Qed.
Class A.
Section Foo.
Variable a : A.
Goal A.
solve [typeclasses eauto].
Undo 1.
clear a.
try typeclasses eauto.
assert(a:=Build_A).
solve [ typeclasses eauto ].
Undo 2.
assert(b:=Build_A).
solve [ typeclasses eauto ].
Qed.
End Foo.
|
