Tests for bugs #3509 and #3510.

3 files changed, 6 insertions, 19 deletions

diff --git a/test-suite/bugs/closed/3509.v b/test-suite/bugs/closed/3509.v
new file mode 100644
index 000000000..822662267
--- /dev/null
+++ b/test-suite/bugs/closed/3509.v
@@ -0,0 +1,6 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 : bar.
+Hint Rewrite a2 : bar.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/closed/3510.v
index daf265071..daf265071 100644
--- a/test-suite/bugs/opened/3510.v
+++ b/test-suite/bugs/closed/3510.v
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
deleted file mode 100644
index 3913bbb43..000000000
--- a/test-suite/bugs/opened/3509.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import TestSuite.admit.
-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.