bug_2149.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_2149.v

blob: 8bc5a2cefcbc247408b3c6d269afab3b1a0fb6c9 (plain)

Lemma Foo : forall x y : nat, y = x -> y = x.
Proof.
intros x y.
rename x into y, y into x.
trivial.
Qed.