diff options
| author | Gaëtan Gilbert | 2019-07-22 13:02:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-22 13:02:02 +0200 |
| commit | 033021860b2ea6fee901f6c760dcd8292ed07fe5 (patch) | |
| tree | e775cbf222039ca80878924529ac21b12fbe66fd /test-suite/success | |
| parent | 21b6ba98b0c0e33ceb106fd164def38d87ff3f0c (diff) | |
| parent | eabe207bc6159f1349f7e6b8e63a55984ea9aa32 (diff) | |
Merge PR #10441: Attach the universe polymorphic status to sections.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: mattam82
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/namedunivs.v | 1 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 9 |
2 files changed, 4 insertions, 6 deletions
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index f9154ef576..01a2136652 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -6,6 +6,7 @@ Unset Strict Universe Declaration. +#[universes(polymorphic)] Section lift_strict. Polymorphic Definition liftlt := let t := Type@{i} : Type@{k} in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 339f798240..9ab8ace39e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -122,8 +122,6 @@ Fail Definition id1impred := ((forall A : Type1, A) : Type1). End Hierarchy. -Section structures. - Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type @@ -154,9 +152,6 @@ Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}. Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. -End structures. - - Module binders. Definition mynat@{|} := nat. @@ -201,7 +196,8 @@ Module binders. Definition with_mono@{u|u < M} : Type@{M} := Type@{u}. End binders. - + +#[universes(polymorphic)] Section cats. Local Set Universe Polymorphism. Require Import Utf8. @@ -307,6 +303,7 @@ Fail Check (let A := Set in fooS (id A)). Fail Check (let A := Prop in fooS (id A)). (* Some tests of sort-polymorphisme *) +#[universes(polymorphic)] Section S. Polymorphic Variable A:Type. (* |