From 5f0a8667e880eeca9e79687091cd8db2256e950c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Feb 2015 11:43:30 +0100
Subject: Test for #2946 (trunk bug with let's in unification).

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

diff --git a/test-suite/bugs/closed/2946.v b/test-suite/bugs/closed/2946.v
new file mode 100644
index 0000000000..d8138e145c
--- /dev/null
+++ b/test-suite/bugs/closed/2946.v
@@ -0,0 +1,8 @@
+Lemma toto (E : nat -> nat -> Prop) (x y : nat)  
+  (Ex_ : forall z, E x z) (E_y : forall z, E z y) : True.
+
+(* OK *)                                                                     
+assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy).               
+
+(* FAIL *)                                                                   
+assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy).
-- 
cgit v1.2.3