aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/clear.v
blob: 976bec73719f267954538e5cf59bcd8e0608c61d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.