aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/clear.v
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.