From 1c620d266885086e076011917d5b1d28af299ea1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Jun 2014 15:46:17 +0200
Subject: Move bug # 3368 to closed bugs

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

diff --git a/test-suite/bugs/closed/3368.v b/test-suite/bugs/closed/3368.v
new file mode 100644
index 0000000000..64fb035681
--- /dev/null
+++ b/test-suite/bugs/closed/3368.v
@@ -0,0 +1,15 @@
+(* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *)
+Set Universe Polymorphism.
+Set Primitive Projections.
+Record PreCategory := { object :> Type; morphism : object -> object -> Type }.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }.
+Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory C (fun s d => morphism C d s).
+Definition opposite' C D (F : Functor C D)
+  := Build_Functor (opposite C) (opposite D)
+                   (object_of F)
+                   (fun s d => @morphism_of C D F d s).
+(* Toplevel input, characters 15-191:
+Anomaly: File "pretyping/reductionops.ml", line 149, characters 4-10: Assertion failed.
+Please report. *)
diff --git a/test-suite/bugs/opened/3368.v b/test-suite/bugs/opened/3368.v
deleted file mode 100644
index c0c00b4edf..0000000000
--- a/test-suite/bugs/opened/3368.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *)
-Set Universe Polymorphism.
-Set Primitive Projections.
-Record PreCategory := { object :> Type; morphism : object -> object -> Type }.
-Record Functor (C D : PreCategory) :=
-  { object_of :> C -> D;
-    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }.
-Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory C (fun s d => morphism C d s).
-Fail Definition opposite' C D (F : Functor C D)
-  := Build_Functor (opposite C) (opposite D)
-                   (object_of F)
-                   (fun s d => @morphism_of C D F s d).
-(* Toplevel input, characters 15-191:
-Anomaly: File "pretyping/reductionops.ml", line 149, characters 4-10: Assertion failed.
-Please report. *)
-- 
cgit v1.2.3