aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Rename.v
blob: 0576f3c68fa336370628e3f7c58a4f6c786b2f5f (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 (#842) *)

Section rename.

Variable A:Prop.

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

End rename.