Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
new file mode 100644
index 00000000..d41d2317
--- /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.