Imported Upstream version 8.5~beta1+dfsg

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
new file mode 100644
index 00000000..bce7c3f2
--- /dev/null
+++ b/test-suite/bugs/opened/3298.v
@@ -0,0 +1,23 @@
+Module JGross.
+  Hint Extern 1 => match goal with |- match ?E with end => case E end.
+
+  Goal forall H : False, match H return Set with end.
+  Proof.
+    intros.
+    Fail solve [ eauto ]. (* No applicable tactic *)
+    admit.
+  Qed.
+End JGross.
+
+Section BenDelaware.
+  Hint Extern 0 => admit.
+  Goal forall (H : False), id (match H return Set with end).
+  Proof.
+    eauto.
+  Qed.
+  Goal forall (H : False), match H return Set with end.
+  Proof.
+    Fail solve [ eauto ] .
+    admit.
+  Qed.
+End BenDelaware.