From c13a3b61c9b1a714c50bcf0ec371a4effe1ff627 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 27 Jun 2019 15:09:40 +0200 Subject: Attach the universe polymorphic status to sections. The previous implementation allowed to dynamically decide whether a section would be monomorphic or polymorphic at the first definition of a variable or a constraint. Instead of relying on this delayed decision, we set the universe polymorphic property directly at the time of the section definition. --- test-suite/bugs/closed/HoTT_coq_020.v | 2 ++ test-suite/bugs/closed/HoTT_coq_098.v | 2 ++ test-suite/bugs/closed/bug_3314.v | 6 +++--- test-suite/bugs/closed/bug_4503.v | 2 ++ test-suite/bugs/closed/bug_4816.v | 5 +++++ 5 files changed, 14 insertions(+), 3 deletions(-) (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 73da464bbe..babd180209 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -26,6 +26,7 @@ Ltac present_obj from to := | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. +#[universes(polymorphic)] Section NaturalTransformationComposition. Set Universe Polymorphism. Context `(C : @Category objC). @@ -58,6 +59,7 @@ Polymorphic Definition Cat0 : Category Empty_set Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). +#[universes(polymorphic)] Section Law0. Polymorphic Variable objC : Type. Polymorphic Variable C : Category objC. diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v index bdcd8ba97d..3b58605575 100644 --- a/test-suite/bugs/closed/HoTT_coq_098.v +++ b/test-suite/bugs/closed/HoTT_coq_098.v @@ -21,6 +21,7 @@ Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex. Admitted. Module success. + #[universes(polymorphic)] Section SpecializedFunctor. Set Universe Polymorphism. Context `(C : @SpecializedCategory objC). @@ -39,6 +40,7 @@ Module success. End success. Module success2. + #[universes(polymorphic)] Section SpecializedFunctor. Polymorphic Context `(C : @SpecializedCategory objC). Polymorphic Context `(D : @SpecializedCategory objD). diff --git a/test-suite/bugs/closed/bug_3314.v b/test-suite/bugs/closed/bug_3314.v index a5782298c3..794de93b37 100644 --- a/test-suite/bugs/closed/bug_3314.v +++ b/test-suite/bugs/closed/bug_3314.v @@ -24,10 +24,10 @@ Fail Eval compute in Lift nat : Prop. (* = nat : Prop *) -Section Hurkens. +Monomorphic Definition Type2 := Type. +Monomorphic Definition Type1 := Type : Type2. - Monomorphic Definition Type2 := Type. - Monomorphic Definition Type1 := Type : Type2. +Section Hurkens. (** Assumption of a retract from Type into Prop *) diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 26731e3292..88391c7bb1 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -5,6 +5,7 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := (* FAILURE 1 *) +#[universes(polymorphic)] Section foo. Polymorphic Universes A. Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. @@ -30,6 +31,7 @@ End ILogic. Set Printing Universes. (* There is still a problem if the class is universe polymorphic *) +#[universes(polymorphic)] Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v index 00a523842e..50cb7d280a 100644 --- a/test-suite/bugs/closed/bug_4816.v +++ b/test-suite/bugs/closed/bug_4816.v @@ -1,3 +1,4 @@ +#[universes(polymorphic)] Section foo. Polymorphic Universes A B. Fail Constraint A <= B. @@ -5,12 +6,14 @@ End foo. (* gives an anomaly Universe undefined *) Universes X Y. +#[universes(polymorphic)] Section Foo. Polymorphic Universes Z W. Polymorphic Constraint W < Z. Fail Definition bla := Type@{W}. Polymorphic Definition bla := Type@{W}. + #[universes(polymorphic)] Section Bar. Fail Constraint X <= Z. End Bar. @@ -21,8 +24,10 @@ Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := { refl : forall x, r x x }. +#[universes(polymorphic)] Section qux. Polymorphic Universes A. + #[universes(polymorphic)] Section bar. Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. -- cgit v1.2.3 From b8f77d00c586fd17c8447ab6fc74acf97b5597c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 12 Jul 2019 16:42:06 +0200 Subject: Polymorphism attribute on section sets the option locally. This is deemed to be more natural as most of the uses will follow this structure. --- test-suite/bugs/closed/bug_4503.v | 4 ++-- test-suite/bugs/closed/bug_4816.v | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 88391c7bb1..c53d4cabc7 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -10,7 +10,7 @@ Section foo. Polymorphic Universes A. Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. - Fail Definition foo := PO. + Fail Monomorphic Definition foo := PO. End foo. @@ -34,6 +34,6 @@ Set Printing Universes. #[universes(polymorphic)] Section Embed_ILogic_Pre. Polymorphic Universes A T. - Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. + Fail Monomorphic Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. End Embed_ILogic_Pre. diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v index 50cb7d280a..0bb05e77ce 100644 --- a/test-suite/bugs/closed/bug_4816.v +++ b/test-suite/bugs/closed/bug_4816.v @@ -1,7 +1,7 @@ #[universes(polymorphic)] Section foo. Polymorphic Universes A B. -Fail Constraint A <= B. +Fail Monomorphic Constraint A <= B. End foo. (* gives an anomaly Universe undefined *) @@ -11,11 +11,11 @@ Section Foo. Polymorphic Universes Z W. Polymorphic Constraint W < Z. - Fail Definition bla := Type@{W}. + Fail Monomorphic Definition bla := Type@{W}. Polymorphic Definition bla := Type@{W}. #[universes(polymorphic)] Section Bar. - Fail Constraint X <= Z. + Fail Monomorphic Constraint X <= Z. End Bar. End Foo. @@ -29,6 +29,6 @@ Section qux. Polymorphic Universes A. #[universes(polymorphic)] Section bar. - Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Monomorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End qux. -- cgit v1.2.3