Move opened bugs to bugs/opened

1 files changed, 0 insertions, 132 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
deleted file mode 100644
index b06830dd0..000000000
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ /dev/null
@@ -1,132 +0,0 @@
-Module Version1.
-  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 *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
-  (* (fun (A : Category (* Top.68 *))
-   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
- {|  |}) SetCat (* Top.68 *)
-     : forall
-         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
-       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
-       SpecializedCategory (* Top.69 *)
-         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
-  Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
-Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
-< Top.51). *)
-End Version1.
-
-Module Version2.
-  Set Implicit Arguments.
-  Set Universe Polymorphism.
-
-  Record SpecializedCategory (obj : Type) :=
-    {
-      Object : _ := obj
-    }.
-
-  Record > Category :=
-    {
-      CObject : Type;
-      UnderlyingCategory :> @SpecializedCategory CObject
-    }.
-
-  Parameter TerminalCategory : SpecializedCategory unit.
-
-  Definition focus A (_ : A) := True.
-  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
-                               (objD : Type) (D : SpecializedCategory objD), Prop.
-  Definition CommaCategory_Object (A : Category) : Type.
-    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    progress change CObject with (fun C => @Object (CObject C) C) in *;
-      simpl in *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Definition Build_SliceCategory := @CommaCategory_Object.
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Check @Build_SliceCategory SetCat.
-End Version2.
-
-Module OtherBug.
-  Set Implicit Arguments.
-  Set Universe Polymorphism.
-
-  Record SpecializedCategory (obj : Type) :=
-    {
-      Object : _ := obj
-    }.
-
-  Record > Category :=
-    {
-      CObject : Type;
-      UnderlyingCategory :> @SpecializedCategory CObject
-    }.
-
-  Parameter TerminalCategory : SpecializedCategory unit.
-
-  Definition focus A (_ : A) := True.
-
-  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
-                               (objD : Type) (D : SpecializedCategory objD), Prop.
-  Definition CommaCategory_Object (A : Category) : Type.
-    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
-    progress change CObject with (fun C => @Object (CObject C) C) in *;
-      simpl in *.
-    match type of Hf with
-      | focus ?V => exact V
-    end.
-  Defined.
-
-  Parameter SetCat : @SpecializedCategory Set.
-
-  Set Printing Universes.
-  Definition Build_SliceCategory := @CommaCategory_Object.
-  Check @CommaCategory_Object SetCat.
-  (* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
-     : Type (* Top.44 *) *)
-  Check @Build_SliceCategory SetCat.
-  (* Toplevel input, characters 0-34:
-Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
-< Top.36). *)
-End OtherBug.