Imported Upstream version 8.5~beta1+dfsg

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
new file mode 100644
index 00000000..02e47a8b
--- /dev/null
+++ b/test-suite/bugs/opened/3509.v
@@ -0,0 +1,18 @@
+Lemma match_bool_fn b A B xT xF
+: match b as b return forall x : A, B b x with
+    | true => xT
+    | false => xF
+  end
+  = fun x : A => match b as b return B b x with
+                   | true => xT x
+                   | false => xF x
+                 end.
+admit.
+Defined.
+Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
+: (if b as b return B (if b then t else f) then F t else F f)
+  = F (if b then t else f).
+admit.
+Defined.
+Hint Rewrite match_bool_fn : matchdb.
+Fail Hint Rewrite match_bool_comm_1 : matchdb.