rename test files (do not start by a digit)

1 files changed, 0 insertions, 70 deletions

diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
deleted file mode 100644
index 38f03b166b..0000000000
--- a/test-suite/bugs/closed/3481.v
+++ /dev/null
@@ -1,70 +0,0 @@
-
-Set Implicit Arguments.
-
-Require Import Logic.
-Module NonPrim.
-Local Set Nonrecursive Elimination Schemes.
-Record prodwithlet (A B : Type) : Type :=
-  pair' { fst : A; fst' := fst; snd : B }.
-
-Definition letreclet (p : prodwithlet nat nat) :=
-  let (x, x', y) := p in x + y.
-
-Definition pletreclet (p : prodwithlet nat nat) :=
-  let 'pair' x x' y := p in x + y + x'.
-
-Definition pletreclet2 (p : prodwithlet nat nat) :=
-  let 'pair' x y := p in x + y.
-
-Check (pair 0 0).
-End NonPrim.
-
-Global Set Universe Polymorphism.
-Global Set Asymmetric Patterns.
-Local Set Nonrecursive Elimination Schemes.
-Local Set Primitive Projections.
-
-Record prod (A B : Type) : Type :=
-  pair { fst : A; snd : B }.
-
-Print prod_rect.
-
-(* What I really want: *)
-Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
-           (p : prod A B) : P p
-  := u (fst p) (snd p).
-
-Definition conv : @prod_rect = @prod_rect'.
-Proof. reflexivity. Defined.
-
-Definition imposs :=
-  (fun A B P f (p : prod A B) => match p as p0 return P p0 with
-                                   | {| fst := x ; snd := x0 |} => f x x0
-                                 end).
-
-Definition letrec (p : prod nat nat) :=
-  let (x, y) := p in x + y.
-Eval compute in letrec (pair 1 5).
-
-Goal forall p : prod nat nat, letrec p = fst p + snd p.
-Proof.
-  reflexivity.
-  Undo.
-  intros p.
-  case p. simpl. unfold letrec. simpl. reflexivity.
-Defined.
-
-Eval compute in conv. (* = eq_refl
-     : prod_rect = prod_rect' *)
-
-Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13:
-Error:
-The term "eq_refl" has type "prod_rect = prod_rect"
-while it is expected to have type "prod_rect = prod_rect'"
-(cannot unify "prod_rect" and "prod_rect'"). *)
-
-Record sigma (A : Type) (B : A -> Type) : Type :=
-  dpair { pi1 : A ; pi2 : B pi1 }.
-
-
-