From d7c8d18cca8a41db7ba12c8f6131e8a42491e962 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Feb 2015 20:36:19 +0100
Subject: Test for bug #3249.

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

diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
new file mode 100644
index 0000000000..d41d231739
--- /dev/null
+++ b/test-suite/bugs/closed/3249.v
@@ -0,0 +1,11 @@
+Set Implicit Arguments.
+
+Ltac ret_and_left T :=
+  let t := type of T in
+  lazymatch eval hnf in t with
+    | ?a /\ ?b => constr:(proj1 T)
+    | forall x : ?T', @?f x =>
+      constr:(fun x : T' => $(let fx := constr:(T x) in
+                              let t := ret_and_left fx in
+                              exact t)$)
+  end.
-- 
cgit v1.2.3