From 9a56644b05248d2068f1c5f804e581bc8a7f7275 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Nov 2014 16:00:04 +0100 Subject: Cleaning up closed bugs in test-suite. --- test-suite/bugs/closed/3686.v | 62 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/3804.v | 12 --------- test-suite/bugs/opened/3684.v | 2 -- test-suite/bugs/opened/3686.v | 61 ------------------------------------------ 4 files changed, 62 insertions(+), 75 deletions(-) create mode 100644 test-suite/bugs/closed/3686.v delete mode 100644 test-suite/bugs/closed/3804.v delete mode 100644 test-suite/bugs/opened/3684.v delete mode 100644 test-suite/bugs/opened/3686.v diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v new file mode 100644 index 0000000000..ee6b334ba2 --- /dev/null +++ b/test-suite/bugs/closed/3686.v @@ -0,0 +1,62 @@ +Set Universe Polymorphism. +Set Implicit Arguments. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Bind Scope category_scope with PreCategory. +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); + identity_of : forall s m, morphism_of s s m = morphism_of s s m }. +Definition sub_pre_cat (P : PreCategory -> Type) : PreCategory. +Proof. + exact (@Build_PreCategory PreCategory Functor). +Defined. +Definition opposite (C : PreCategory) : PreCategory. +Proof. + exact (@Build_PreCategory C (fun s d => morphism C d s)). +Defined. +Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope. +Definition prod (C D : PreCategory) : PreCategory. +Proof. + refine (@Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)). +Defined. +Local Infix "*" := prod : category_scope. +Axiom functor_category : PreCategory -> PreCategory -> PreCategory. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Module Export PointwiseCore. + Definition pointwise + (C C' : PreCategory) + (F : Functor C' C) + (D D' : PreCategory) + (G : Functor D D') + : Functor (C -> D) (C' -> D'). + Proof. + refine (Build_Functor + (C -> D) (C' -> D') + _ + _ + _); + abstract admit. + Defined. +End PointwiseCore. +Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G. +Local Open Scope category_scope. +Definition functor_uncurried (P : PreCategory -> Type) + (has_functor_categories : forall C D : @sub_pre_cat P, P (C -> D)) +: object (((@sub_pre_cat P)^op * (@sub_pre_cat P)) -> (@sub_pre_cat P)). +Proof. + pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => Pidentity_of _ _)) || fail "early". + Include PointwiseCore. + pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => Pidentity_of _ _)). +Abort. diff --git a/test-suite/bugs/closed/3804.v b/test-suite/bugs/closed/3804.v deleted file mode 100644 index 5dc0f72642..0000000000 --- a/test-suite/bugs/closed/3804.v +++ /dev/null @@ -1,12 +0,0 @@ -Set Universe Polymorphism. -Module Foo. - Definition T : sigT (fun x => x). - Proof. - exists Set. - abstract exact nat. - Defined. -End Foo. -Module Bar. - Include Foo. -End Bar. -Definition foo := eq_refl : Foo.T = Bar.T. (* Error: Conversion test raised an anomaly *) \ No newline at end of file diff --git a/test-suite/bugs/opened/3684.v b/test-suite/bugs/opened/3684.v deleted file mode 100644 index e32a51223c..0000000000 --- a/test-suite/bugs/opened/3684.v +++ /dev/null @@ -1,2 +0,0 @@ -Definition foo : Set. - Fail refine ($(abstract admit)$). diff --git a/test-suite/bugs/opened/3686.v b/test-suite/bugs/opened/3686.v deleted file mode 100644 index 5f76fc9907..0000000000 --- a/test-suite/bugs/opened/3686.v +++ /dev/null @@ -1,61 +0,0 @@ -Set Universe Polymorphism. -Set Implicit Arguments. -Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. -Bind Scope category_scope with PreCategory. -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); - identity_of : forall s m, morphism_of s s m = morphism_of s s m }. -Definition sub_pre_cat (P : PreCategory -> Type) : PreCategory. -Proof. - exact (@Build_PreCategory PreCategory Functor). -Defined. -Definition opposite (C : PreCategory) : PreCategory. -Proof. - exact (@Build_PreCategory C (fun s d => morphism C d s)). -Defined. -Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope. -Definition prod (C D : PreCategory) : PreCategory. -Proof. - refine (@Build_PreCategory - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)). -Defined. -Local Infix "*" := prod : category_scope. -Axiom functor_category : PreCategory -> PreCategory -> PreCategory. -Local Notation "C -> D" := (functor_category C D) : category_scope. -Module Export PointwiseCore. - Definition pointwise - (C C' : PreCategory) - (F : Functor C' C) - (D D' : PreCategory) - (G : Functor D D') - : Functor (C -> D) (C' -> D'). - Proof. - refine (Build_Functor - (C -> D) (C' -> D') - _ - _ - _); - abstract admit. - Defined. -End PointwiseCore. -Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G. -Local Open Scope category_scope. -Definition functor_uncurried (P : PreCategory -> Type) - (has_functor_categories : forall C D : @sub_pre_cat P, P (C -> D)) -: object (((@sub_pre_cat P)^op * (@sub_pre_cat P)) -> (@sub_pre_cat P)). -Proof. - pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) - in Build_Functor - ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) - object_of - (fun CD C'D' FG => pointwise (fst FG) (snd FG)) - (fun _ _ => Pidentity_of _ _)) || fail "early". - Include PointwiseCore. - Fail pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) - in Build_Functor - ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) - object_of - (fun CD C'D' FG => pointwise (fst FG) (snd FG)) - (fun _ _ => Pidentity_of _ _)). -- cgit v1.2.3