rename test files (do not start by a digit)

1 files changed, 0 insertions, 209 deletions

diff --git a/test-suite/bugs/closed/3422.v b/test-suite/bugs/closed/3422.v
deleted file mode 100644
index 460ae8f110..0000000000
--- a/test-suite/bugs/closed/3422.v
+++ /dev/null
@@ -1,209 +0,0 @@
-Require Import TestSuite.admit.
-Generalizable All Variables.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Axiom admit : forall {T}, T.
-Reserved Infix "o" (at level 40, left associativity).
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
-Existing Instance equiv_isequiv.
-Delimit Scope equiv_scope with equiv.
-Local Open Scope equiv_scope.
-Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
-Axiom IsHSet : Type -> Type.
-Existing Class IsHSet.
-Definition trunc_equiv' `(f : A <~> B) `{IsHSet A} : IsHSet B := admit.
-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);
-
-    trunc_morphism : forall s d, IsHSet (morphism s d) }.
-
-Bind Scope category_scope with PreCategory.
-Infix "o" := (@compose _ _ _ _) : morphism_scope.
-
-Delimit Scope functor_scope with functor.
-
-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)
-  }.
-
-Bind Scope functor_scope with Functor.
-Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
-Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
-Local Open Scope morphism_scope.
-
-Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
-
-Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
-
-Class Isomorphic {C : PreCategory} s d :=
-  {
-    morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
-  }.
-
-Coercion morphism_isomorphic : Isomorphic >-> morphism.
-
-Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
-
-Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}.
-
-Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1)
-: IsIsomorphism (m0 o m1).
-admit.
-Defined.
-
-Section composition.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable E : PreCategory.
-  Variable G : Functor D E.
-  Variable F : Functor C D.
-
-  Definition composeF : Functor C E
-    := Build_Functor
-         C E
-         (fun c => G (F c))
-         (fun _ _ m => morphism_of G (morphism_of F m)).
-End composition.
-Infix "o" := composeF : functor_scope.
-
-Delimit Scope natural_transformation_scope with natural_transformation.
-Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
-
-Section compose.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variables F F' F'' : Functor C D.
-
-  Variable T' : NaturalTransformation F' F''.
-  Variable T : NaturalTransformation F F'.
-
-  Local Notation CO c := (T' c o T c).
-
-  Definition composeT
-  : NaturalTransformation F F'' := Build_NaturalTransformation F F'' (fun c => CO c).
-
-End compose.
-
-Section whisker.
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variable E : PreCategory.
-
-  Section L.
-    Variable F : Functor D E.
-    Variables G G' : Functor C D.
-    Variable T : NaturalTransformation G G'.
-
-    Local Notation CO c := (morphism_of F (T c)).
-
-    Definition whisker_l
-      := Build_NaturalTransformation
-           (F o G) (F o G')
-           (fun c => CO c).
-
-  End L.
-
-  Section R.
-    Variables F F' : Functor D E.
-    Variable T : NaturalTransformation F F'.
-    Variable G : Functor C D.
-
-    Local Notation CO c := (T (G c)).
-
-    Definition whisker_r
-      := Build_NaturalTransformation
-           (F o G) (F' o G)
-           (fun c => CO c).
-  End R.
-End whisker.
-Infix "o" := composeT : natural_transformation_scope.
-Infix "oL" := whisker_l (at level 40, left associativity) : natural_transformation_scope.
-Infix "oR" := whisker_r (at level 40, left associativity) : natural_transformation_scope.
-
-Section path_natural_transformation.
-
-  Variable C : PreCategory.
-  Variable D : PreCategory.
-  Variables F G : Functor C D.
-
-  Lemma equiv_sig_natural_transformation
-  : { CO : forall x, morphism D (F x) (G x)
-    | forall s d (m : morphism C s d),
-        CO d o F _1 m = G _1 m o CO s }
-      <~> NaturalTransformation F G.
-    admit.
-  Defined.
-
-  Global Instance trunc_natural_transformation
-  : IsHSet (NaturalTransformation F G).
-  Proof.
-    eapply trunc_equiv'; [ exact equiv_sig_natural_transformation | ].
-    admit.
-  Qed.
-
-End path_natural_transformation.
-Definition functor_category (C D : PreCategory) : PreCategory
-  := @Build_PreCategory (Functor C D) (@NaturalTransformation C D) (@composeT C D) _.
-
-Notation "C -> D" := (functor_category C D) : category_scope.
-
-Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G.
-
-Coercion natural_transformation_of_natural_isomorphism C D F G (T : @NaturalIsomorphism C D F G) : NaturalTransformation F G
-  := T : morphism _ _ _.
-Local Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
-Global Instance isisomorphism_compose'
-       `(T' : @NaturalTransformation C D F' F'')
-       `(T : @NaturalTransformation C D F F')
-       `{@IsIsomorphism (C -> D) F' F'' T'}
-       `{@IsIsomorphism (C -> D) F F' T}
-: @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
-  := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
-
-Section lemmas.
-  Local Open Scope natural_transformation_scope.
-
-  Variable C : PreCategory.
-  Variable F : C -> PreCategory.
-  Context
-    {w x y z}
-    {f : Functor (F w) (F z)} {f0 : Functor (F w) (F y)}
-    {f1 : Functor (F x) (F y)} {f2 : Functor (F y) (F z)}
-    {f3 : Functor (F w) (F x)} {f4 : Functor (F x) (F z)}
-    {f5 : Functor (F w) (F z)} {n : f5 <~=~> (f4 o f3)%functor}
-    {n0 : f4 <~=~> (f2 o f1)%functor} {n1 : f0 <~=~> (f1 o f3)%functor}
-    {n2 : f <~=~> (f2 o f0)%functor}.
-
-  Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper'
-  : @IsIsomorphism
-      (_ -> _) _ _
-      (n2 ^-1 o (f2 oL n1 ^-1 o (admit o (n0 oR f3 o n))))%natural_transformation.
-  Proof.
-    eapply isisomorphism_compose';
-    [ eapply isisomorphism_inverse
-    | eapply isisomorphism_compose';
-      [ admit
-      | eapply isisomorphism_compose';
-        [ admit |
-          eapply isisomorphism_compose'; [ admit | ]]]].
-    Set Printing All. Set Printing Universes.
-    apply @isisomorphism_isomorphic.
-  Qed.
-
-End lemmas.