Move opened bugs to bugs/opened

1 files changed, 0 insertions, 187 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
deleted file mode 100644
index fae954f81..000000000
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ /dev/null
@@ -1,187 +0,0 @@
-(* File reduced by coq-bug-finder from 279 lines to 219 lines. *)
-
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Definition admit {T} : T.
-Admitted.
-Module Export Overture.
-  Reserved Notation "g 'o' f" (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.
-
-  Delimit Scope path_scope with path.
-
-  Local Open Scope path_scope.
-
-  Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
-    := match p with idpath => idpath end.
-
-  Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
-  : forall x, f x = g x
-    := fun x => match h with idpath => idpath end.
-
-  Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
-
-  Delimit Scope equiv_scope with equiv.
-  Local Open Scope equiv_scope.
-
-  Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
-
-  Class Funext :=
-    { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
-
-  Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
-    (forall x, f x = g x) -> f = g
-    :=
-      (@apD10 A P f g)^-1.
-
-End Overture.
-
-Module Export Core.
-
-  Set Implicit Arguments.
-  Delimit Scope morphism_scope with morphism.
-  Delimit Scope category_scope with category.
-  Delimit Scope object_scope with object.
-
-  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);
-
-      associativity : forall x1 x2 x3 x4
-                             (m1 : morphism x1 x2)
-                             (m2 : morphism x2 x3)
-                             (m3 : morphism x3 x4),
-                        (m3 o m2) o m1 = m3 o (m2 o m1)
-    }.
-  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.
-
-End Core.
-
-Local Open Scope morphism_scope.
-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)
-  }.
-
-Inductive Unit : Set :=
-  tt : Unit.
-
-Definition indiscrete_category (X : Type) : PreCategory
-  := @Build_PreCategory X
-                        (fun _ _ => Unit)
-                        (fun _ _ _ _ _ => tt)
-                        (fun _ _ _ _ _ _ _ => idpath).
-
-
-Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
-Section path_natural_transformation.
-  Context `{Funext}.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variables F G : Functor C D.
-
-  Section path.
-    Variables T U : NaturalTransformation F G.
-    Lemma path'_natural_transformation
-    : components_of T = components_of U
-      -> T = U.
-      admit.
-    Defined.
-    Lemma path_natural_transformation
-    : (forall x, T x = U x)
-      -> T = U.
-    Proof.
-      intros.
-      apply path'_natural_transformation.
-      apply path_forall; assumption.
-    Qed.
-  End path.
-End path_natural_transformation.
-Ltac path_natural_transformation :=
-  repeat match goal with
-           | _ => intro
-           | _ => apply path_natural_transformation; simpl
-         end.
-Definition comma_category A B C (S : Functor A C) (T : Functor B C)
-: PreCategory.
-  admit.
-Defined.
-Definition compose C D (F F' F'' : Functor C D)
-           (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
-: NaturalTransformation F F''
-  := Build_NaturalTransformation F F''
-                                 (fun c => T' c o T c).
-
-Infix "o" := compose : natural_transformation_scope.
-
-Local Open Scope natural_transformation_scope.
-
-Definition associativity `{fs : Funext}
-           C D F G H I
-           (V : @NaturalTransformation C D F G)
-           (U : @NaturalTransformation C D G H)
-           (T : @NaturalTransformation C D H I)
-: (T o U) o V = T o (U o V).
-Proof.
-  path_natural_transformation.
-
-  apply associativity.
-Qed.
-Definition functor_category `{Funext} (C D : PreCategory) : PreCategory
-  := @Build_PreCategory (Functor C D)
-                        (@NaturalTransformation C D)
-                        (@compose C D)
-                        (@associativity _ C D).
-
-Notation "C -> D" := (functor_category C D) : category_scope.
-
-Definition compose_functor `{Funext} (C D E : PreCategory) : object ((C -> D) -> ((D -> E) -> (C -> E))).
-  admit.
-
-Defined.
-
-Definition pullback_along `{Funext} (C C' D : PreCategory) (p : Functor C C')
-: object ((C' -> D) -> (C -> D))
-  := Eval hnf in compose_functor _ _ _ p.
-
-Definition IsColimit `{Funext} C D (F : Functor D C) (x : object
-                                                            (@comma_category (indiscrete_category Unit)
-                                                                             (@functor_category H (indiscrete_category Unit) C)
-                                                                             (@functor_category H D C)
-                                                                             admit
-                                                                             (@pullback_along H D (indiscrete_category Unit) C
-                                                                                              admit))) : Type
-  := admit.
-
-Generalizable All Variables.
-Axiom fs : Funext.
-
-Section bar.
-
-  Variable D : PreCategory.
-
-  Context `(has_colimits
-            : forall F : Functor D C,
-                @IsColimit _ C D F (colimits F)).
-(* Error: Unsatisfied constraints: Top.3773 <= Set
- (maybe a bugged tactic). *)