From bc7d29e4c0f53d5c8e654157c4137c7e82910a7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 17:22:41 +0100
Subject: Test for bug #3298.

---
 test-suite/bugs/closed/3298.v | 21 +++++++++++++++++++++
 test-suite/bugs/opened/3298.v | 23 -----------------------
 2 files changed, 21 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/3298.v
 delete mode 100644 test-suite/bugs/opened/3298.v

(limited to 'test-suite')

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.
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
deleted file mode 100644
index bce7c3f23b..0000000000
--- a/test-suite/bugs/opened/3298.v
+++ /dev/null
@@ -1,23 +0,0 @@
-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.
-- 
cgit v1.2.3