From c96bde02138e00ba8800733e4ca2f1915b4c0c6f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Nov 2014 11:51:52 +0100
Subject: Adding test for bug #3248.

---
 test-suite/bugs/opened/3248.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/opened/3248.v

diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
new file mode 100644
index 0000000000..714df5ccae
--- /dev/null
+++ b/test-suite/bugs/opened/3248.v
@@ -0,0 +1,17 @@
+Ltac ret_and_left f :=
+  let tac := ret_and_left in
+  let T := type of f in
+  lazymatch eval hnf in T with
+    | ?T' -> _ =>
+      let ret := constr:(fun x' : T' => $(tac (f x'))$) in
+      exact ret
+    | ?T' => exact f
+  end.
+
+Goal forall A B : Prop, forall x y : A, True.
+Proof.
+  intros A B x y.
+  pose (f := fun (x y : A) => conj x y).
+  pose (a := $(ret_and_left f)$).
+  unify (a x y) (conj x y).
+Abort.
-- 
cgit v1.2.3