From 4586e904f8d2759c4f19e1ac3ad5c0447b353ae0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Nov 2014 02:36:19 +0100
Subject: Test for bug #3487.

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

diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v
new file mode 100644
index 0000000000..ba7a5c98fc
--- /dev/null
+++ b/test-suite/bugs/closed/3487.v
@@ -0,0 +1,8 @@
+Notation bar := $(exact I)$.
+Notation foo := bar (only parsing).
+Class baz := { x : False }.
+Instance: baz.
+Admitted.
+Definition baz0 := ((_ : baz) = (_ : baz)).
+Definition foo1 := (foo = foo).
+Fail Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
diff --git a/test-suite/bugs/opened/3487.v b/test-suite/bugs/opened/3487.v
deleted file mode 100644
index ba7a5c98fc..0000000000
--- a/test-suite/bugs/opened/3487.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Notation bar := $(exact I)$.
-Notation foo := bar (only parsing).
-Class baz := { x : False }.
-Instance: baz.
-Admitted.
-Definition baz0 := ((_ : baz) = (_ : baz)).
-Definition foo1 := (foo = foo).
-Fail Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
-- 
cgit v1.2.3