Move opened bugs to bugs/opened

1 files changed, 0 insertions, 126 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
deleted file mode 100644
index d1ea16ec3..000000000
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ /dev/null
@@ -1,126 +0,0 @@
-(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines. *)
-
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Definition admit {T} : T.
-Admitted.
-Delimit Scope object_scope with object.
-Delimit Scope morphism_scope with morphism.
-Delimit Scope category_scope with category.
-Delimit Scope functor_scope with functor.
-Delimit Scope natural_transformation_scope with natural_transformation.
-Reserved Infix "o" (at level 40, left associativity).
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-
-Arguments idpath {A a} , [A] a.
-Notation "x = y :> A" := (@paths A x y) : type_scope.
-Notation "x = y" := (x = y :>_) : type_scope.
-Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
-  := match p with idpath => idpath end.
-
-Record PreCategory :=
-  {
-    Object :> Type;
-    Morphism : Object -> Object -> Type;
-
-    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g)
-  }.
-Bind Scope category_scope with PreCategory.
-
-Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
-
-Infix "o" := Compose : morphism_scope.
-Local Open Scope morphism_scope.
-
-Record Functor (C D : PreCategory) :=
-  {
-    ObjectOf :> C -> D;
-    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
-    FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
-                       MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1)
-  }.
-
-Bind Scope functor_scope with Functor.
-
-Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
-
-Definition ComposeFunctors C D E
-           (G : Functor D E) (F : Functor C D) : Functor C E
-  := Build_Functor C E
-                   (fun c => G (F c))
-                   admit
-                   admit.
-
-Infix "o" := ComposeFunctors : functor_scope.
-
-Record NaturalTransformation C D (F G : Functor C D) :=
-  {
-    ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
-    Commutes : forall s d (m : C.(Morphism) s d),
-                 ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s
-  }.
-
-Generalizable All Variables.
-
-Section NTComposeT.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-
-  Variables F F' F'' : Functor C D.
-
-  Variable T' : NaturalTransformation F' F''.
-  Variable T : NaturalTransformation F F'.
-  Let CO := fun c => T' c o T c.
-  Definition NTComposeT_Commutes s d (m : Morphism C s d)
-  : CO d o MorphismOf F m = MorphismOf F'' m o CO s.
-
-    admit.
-  Defined.
-  Definition NTComposeT
-  : NaturalTransformation F F''
-    := Build_NaturalTransformation F F''
-                                   (fun c => T' c o T c)
-                                   NTComposeT_Commutes.
-End NTComposeT.
-Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
-           (G : Functor C D)
-  := Build_NaturalTransformation (F o G) (F' o G)
-                                 (fun c => T (G c))
-                                 admit.
-Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
-
-Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
-Notation "T 'o' U"
-  := (@NTC_Composable_term _ _ T%natural_transformation U%natural_transformation _ _ _)
-     : natural_transformation_scope.
-
-Local Open Scope natural_transformation_scope.
-
-Lemma NTWhiskerR_CompositionOf C D
-      (F G H : Functor C D)
-      (T : NaturalTransformation G H)
-      (T' : NaturalTransformation F G) B (I : Functor B C)
-: NTWhiskerR (NTComposeT T T') I = NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I).
-
-  admit.
-Defined.
-Definition FunctorCategory C D : PreCategory
-  := @Build_PreCategory (Functor C D)
-                        (NaturalTransformation (C := C) (D := D))
-                        admit.
-
-Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
-
-Variable C : PreCategory.
-Variable D : PreCategory.
-Variable E : PreCategory.
-Definition NTWhiskerR_Functorial (G : [C, D]%category)
-: [[D, E], [C, E]]%category
-  := Build_Functor
-       [C, D] [C, E]
-       (fun F => F o G)
-       (fun _ _ T => T o G)
-       (fun _ _ _ _ _ => inverse (NTWhiskerR_CompositionOf _ _ _)).
-(* Anomaly: Uncaught exception Not_found(_). Please report. *)