aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-27 20:36:19 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-27 20:36:19 +0100
commitd7c8d18cca8a41db7ba12c8f6131e8a42491e962 (patch)
tree1b3bda0c18e0cf81d54cbf52f03a7226d3d7296a /test-suite
parent64a139406409084f25d3ce35e0fa71bbccc63a20 (diff)
Test for bug #3249.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/3249.v11
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 000000000..d41d23173
--- /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.