Move opened bugs to bugs/opened

1 files changed, 0 insertions, 50 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
deleted file mode 100644
index a14fb6aa5..000000000
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
-Set Printing Universes.
-Set Implicit Arguments.
-Generalizable All Variables.
-Set Asymmetric Patterns.
-Set Universe Polymorphism.
-
-Inductive Unit : Type :=
-    tt : Unit.
-
-Inductive Bool : Type :=
-  | true : Bool
-  | false : Bool.
-
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Record PreCategory :=
-  {
-    Object :> Type;
-    Morphism : Object -> Object -> Type
-  }.
-
-Definition DiscreteCategory X : PreCategory
-  := @Build_PreCategory X
-                        (@paths X).
-
-Definition IndiscreteCategory X : PreCategory
-  := @Build_PreCategory X
-                         (fun _ _ => Unit).
-
-Definition NatCategory (n : nat) :=
-  match n with
-    | 0 => IndiscreteCategory Unit
-    | _ => DiscreteCategory Bool
-  end.
-(* Error: Universe inconsistency (cannot enforce Set <= Prop).*)
-
-Definition NatCategory' (n : nat) :=
-  match n with
-    | 0 => (fun X => @Build_PreCategory X
-                         (fun _ _ => Unit : Prop)) Unit
-    | _ => DiscreteCategory Bool
-  end.
-
-Definition NatCategory'' (n : nat) :=
-  match n with
-    | 0 => IndiscreteCategory Unit
-    | _ => DiscreteCategory Bool
-  end.