From f839f718fc6271aeb014c9cb5abdf9106b1c26be Mon Sep 17 00:00:00 2001
From: Xavier Clerc
Date: Tue, 25 Nov 2014 17:11:40 +0100
Subject: Bug #3804 is actually closed (thanks to Jason Gross for the
 notification).

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

diff --git a/test-suite/bugs/closed/3804.v b/test-suite/bugs/closed/3804.v
new file mode 100644
index 0000000000..da9290cbad
--- /dev/null
+++ b/test-suite/bugs/closed/3804.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+Module Foo.
+  Definition T : sigT (fun x => x).
+  Proof.
+    exists Set.
+    abstract exact nat.
+  Defined.
+End Foo.
+Module Bar.
+  Include Foo.
+End Bar.
+Definition foo := eq_refl : Foo.T = Bar.T.
diff --git a/test-suite/bugs/opened/3804.v b/test-suite/bugs/opened/3804.v
deleted file mode 100644
index da9290cbad..0000000000
--- a/test-suite/bugs/opened/3804.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Set Universe Polymorphism.
-Module Foo.
-  Definition T : sigT (fun x => x).
-  Proof.
-    exists Set.
-    abstract exact nat.
-  Defined.
-End Foo.
-Module Bar.
-  Include Foo.
-End Bar.
-Definition foo := eq_refl : Foo.T = Bar.T.
-- 
cgit v1.2.3