Imported Upstream version 8.5~beta1+dfsg

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
new file mode 100644
index 00000000..25285636
--- /dev/null
+++ b/test-suite/bugs/opened/3510.v
@@ -0,0 +1,34 @@
+Lemma match_option_fn T (b : option T) A B s n
+: match b as b return forall x : A, B b x with
+    | Some k => s k
+    | None => n
+  end
+  = fun x : A => match b as b return B b x with
+                   | Some k => s k x
+                   | None => n x
+                 end.
+admit.
+Defined.
+Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
+: match p as p return R match p with
+                          | Some k => s1 k
+                          | None => n1
+                        end
+                        match p as p return B match p with Some k => s1 k | None => n1 end with
+                          | Some k => s2 k
+                          | None => n2
+                        end with
+    | Some k => f (s1 k) (s2 k)
+    | None => f n1 n2
+  end
+  = f match p return A with
+        | Some k => s1 k
+        | None => n1
+      end
+      match p as p return B match p with Some k => s1 k | None => n1 end with
+        | Some k => s2 k
+        | None => n2
+      end.
+admit.
+Defined.
+Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.