diff options
author | 2015-05-18 16:59:50 +0200 | |
---|---|---|
committer | 2015-05-18 16:59:50 +0200 | |
commit | b994685d85d30f0db8ee0ec10f802f6bf3797e4b (patch) | |
tree | 5cfcb3213b27a38fcd953da9ee04b947830a1230 | |
parent | 923ce36ed6789718746369847f622b17bb37df2a (diff) |
Removing test for opened bugs that were already present in the closed test-suite.
-rw-r--r-- | test-suite/bugs/opened/3045.v | 30 | ||||
-rw-r--r-- | test-suite/bugs/opened/3326.v | 18 | ||||
-rw-r--r-- | test-suite/bugs/opened/3562.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/opened/3657.v | 33 | ||||
-rw-r--r-- | test-suite/bugs/opened/3670.v | 19 | ||||
-rw-r--r-- | test-suite/bugs/opened/3675.v | 20 | ||||
-rw-r--r-- | test-suite/bugs/opened/3788.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/opened/3808.v | 2 |
8 files changed, 0 insertions, 129 deletions
diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v deleted file mode 100644 index b7f40b4ad..000000000 --- a/test-suite/bugs/opened/3045.v +++ /dev/null @@ -1,30 +0,0 @@ -Set Asymmetric Patterns. -Generalizable All Variables. -Set Implicit Arguments. -Set Universe Polymorphism. - -Record SpecializedCategory (obj : Type) := - { - Object :> _ := obj; - Morphism : obj -> obj -> Type; - - Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' - }. - -Arguments Compose {obj} [C s d d'] m1 m2 : rename. - -Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := -| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. - -Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d := - match m in @ReifiedMorphism objC C s d return Morphism C s d with - | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1) - (@ReifiedMorphismDenote _ _ _ _ m2) - end. - -Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d) -: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }. -refine match m with - | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _ - end; clear m. -Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ]. diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v deleted file mode 100644 index f73117a2e..000000000 --- a/test-suite/bugs/opened/3326.v +++ /dev/null @@ -1,18 +0,0 @@ -Class ORDER A := Order { - LEQ : A -> A -> bool; - leqRefl: forall x, true = LEQ x x -}. - -Section XXX. - -Variable A:Type. -Variable (O:ORDER A). -Definition aLeqRefl := @leqRefl _ O. - -Lemma OK : forall x, true = LEQ x x. - intros. - unfold LEQ. - destruct O. - clear. - Fail apply aLeqRefl. (* Toplevel input, characters 15-30: -Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v deleted file mode 100644 index 04a1223b6..000000000 --- a/test-suite/bugs/opened/3562.v +++ /dev/null @@ -1,2 +0,0 @@ -Theorem t: True. -Fail destruct 0 as x. diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v deleted file mode 100644 index 6faec0765..000000000 --- a/test-suite/bugs/opened/3657.v +++ /dev/null @@ -1,33 +0,0 @@ -(* Set Primitive Projections. *) -Class foo {A} {a : A} := { bar := a; baz : bar = bar }. -Arguments bar {_} _ {_}. -Instance: forall A a, @foo A a. -intros; constructor. -abstract reflexivity. -Defined. -Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat. -Proof. - Check (bar Set). - Check (bar (fun _ : Set => Set)). - Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *) - -Abort. - - -Module A. -Universes i j. -Constraint i < j. -Variable foo : Type@{i}. -Goal Type@{i}. - Fail let t := constr:(Type@{j}) in - change Type with t. -Abort. - -Goal Type@{j}. - Fail let t := constr:(Type@{i}) in - change Type with t. - let t := constr:(Type@{i}) in - change t. exact foo. -Defined. - -End A. diff --git a/test-suite/bugs/opened/3670.v b/test-suite/bugs/opened/3670.v deleted file mode 100644 index cf5e9b090..000000000 --- a/test-suite/bugs/opened/3670.v +++ /dev/null @@ -1,19 +0,0 @@ -Module Type FOO. - Parameters P Q : Type -> Type. -End FOO. - -Module Type BAR. - Declare Module Export foo : FOO. - Parameter f : forall A, P A -> Q A -> A. -End BAR. - -Module Type BAZ. - Declare Module Export foo : FOO. - Parameter g : forall A, P A -> Q A -> A. -End BAZ. - -Module BAR_FROM_BAZ (baz : BAZ) : BAR. - Import baz. - Module foo <: FOO := foo. - Definition f : forall A, P A -> Q A -> A := g. -End BAR_FROM_BAZ. diff --git a/test-suite/bugs/opened/3675.v b/test-suite/bugs/opened/3675.v deleted file mode 100644 index 93227ab85..000000000 --- a/test-suite/bugs/opened/3675.v +++ /dev/null @@ -1,20 +0,0 @@ -Set Primitive Projections. -Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end. -Notation "p @ q" := (concat p q) (at level 20) : path_scope. -Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y. -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope path_scope. -Local Open Scope equiv_scope. -Generalizable Variables A B C f g. -Lemma isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} -: IsEquiv (compose g f). -Proof. - refine (Build_IsEquiv A C - (compose g f) - (compose f^-1 g^-1) _). - exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)). diff --git a/test-suite/bugs/opened/3788.v b/test-suite/bugs/opened/3788.v deleted file mode 100644 index 8e605a00f..000000000 --- a/test-suite/bugs/opened/3788.v +++ /dev/null @@ -1,5 +0,0 @@ -Set Implicit Arguments. -Global Set Primitive Projections. -Record Functor (C D : Type) := { object_of :> forall _ : C, D }. -Axiom path_functor_uncurried : forall C D (F G : Functor C D) (_ : sigT (fun HO : object_of F = object_of G => Set)), F = G. -Fail Lemma path_functor_uncurried_snd C D F G HO HM : (@path_functor_uncurried C D F G (existT _ HO HM)) = HM. diff --git a/test-suite/bugs/opened/3808.v b/test-suite/bugs/opened/3808.v deleted file mode 100644 index df40ca191..000000000 --- a/test-suite/bugs/opened/3808.v +++ /dev/null @@ -1,2 +0,0 @@ -Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) - := foo : Foo. |