From a33d1c239f2726dbf31e35db29cad08d9e196277 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Nov 2014 00:07:32 +0100
Subject: Test for bug #2149.

---
 test-suite/bugs/closed/2149.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/2149.v

diff --git a/test-suite/bugs/closed/2149.v b/test-suite/bugs/closed/2149.v
new file mode 100644
index 0000000000..38c5f36ab2
--- /dev/null
+++ b/test-suite/bugs/closed/2149.v
@@ -0,0 +1,7 @@
+Lemma Foo : forall x y : nat, y = x -> y = x.
+Proof.
+intros x y.
+rename x into y, y into x.
+trivial.
+Qed.
+
-- 
cgit v1.2.3