2149.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 38c5f36ab23b885eda500b80da0f6c2afae7d875 (plain)

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