Adding test for bug #3248.

1 files changed, 17 insertions, 0 deletions

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.