diff options
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. (* |