aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Rename.v
blob: 2789c6c9a6c791d8b332c8fb667751c839bcb35d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Goal forall n : nat, n = 0 -> n = 0.
intros.
rename n into p.
induction p; auto.
Qed.

(* Submitted by Iris Loeb (BZ#842) *)

Section rename.

Variable A:Prop.

Lemma Tauto: A->A.
rename A into B.
tauto.
Qed.

End rename.