test-suite/success/Rename.v


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.