Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v
new file mode 100644
index 00000000..f07ee1e6
--- /dev/null
+++ b/test-suite/bugs/closed/3298.v
@@ -0,0 +1,22 @@
+Require Import TestSuite.admit.
+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.