Move opened bugs to bugs/opened

1 files changed, 0 insertions, 50 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_045.v b/test-suite/bugs/closed/HoTT_coq_045.v
deleted file mode 100644
index 590bdd157..000000000
--- a/test-suite/bugs/closed/HoTT_coq_045.v
+++ /dev/null
@@ -1,50 +0,0 @@
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Generalizable All Variables.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj
-  }.
-
-Record > Category :=
-  {
-    CObject : Type;
-    UnderlyingCategory :> @SpecializedCategory CObject
-  }.
-
-Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
-  {
-    ObjectOf :> objC -> objD
-  }.
-
-Definition Functor (C D : Category) := SpecializedFunctor C D.
-
-Parameter TerminalCategory : SpecializedCategory unit.
-
-Definition focus A (_ : A) := True.
-
-Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
-  assert (Hf : focus ((S tt) = (S tt))) by constructor.
-  progress change CObject with (fun C => @Object (CObject C) C) in *.
-  simpl in *.
-  let V := match type of Hf with
-             | focus ?V => constr:(V)
-           end
-  in exact V.
-(* Toplevel input, characters 89-96:
-Error: Illegal application:
-The term "ObjectOf" of type
- "forall (objC : Set) (C : SpecializedCategory objC)
-    (objD : Type) (D : SpecializedCategory objD),
-  SpecializedFunctor C D -> objC -> objD"
-cannot be applied to the terms
- "Object TerminalCategory" : "Type"
- "TerminalCategory" : "SpecializedCategory unit"
- "Object A" : "Type"
- "UnderlyingCategory A" : "SpecializedCategory (CObject A)"
- "S" : "Functor TerminalCategory A"
- "tt" : "unit"
-The 1st term has type "Type" which should be coercible to
-"Set". *)
-Defined.