Test for bug #3298.

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v
new file mode 100644
index 0000000000..3a7de45670
--- /dev/null
+++ b/test-suite/bugs/closed/3298.v
@@ -0,0 +1,21 @@
+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.
+    solve [ eauto ].
+  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.
+    solve [ eauto ] .
+  Qed.
+End BenDelaware.