diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Template.v | 4 | ||||
| -rw-r--r-- | test-suite/success/attribute_syntax.v | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index 1c6e2d81d8..cfc25c3346 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -25,7 +25,7 @@ Module AutoNo. End AutoNo. Module Yes. - #[template] + #[universes(template)] Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A. About Box. @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[notemplate] + #[universes(notemplate)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index 7b972f4ed9..f4f59a3c16 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -11,7 +11,7 @@ End Scope. Fail Check 0 = true :> nat. -#[polymorphic] +#[universes(polymorphic)] Definition ι T (x: T) := x. Check ι _ ι. @@ -24,9 +24,9 @@ Reset f. Ltac foo := foo. Module M. - #[local] #[polymorphic] Definition zed := Type. + #[local] #[universes(polymorphic)] Definition zed := Type. - #[local, polymorphic] Definition kats := Type. + #[local, universes(polymorphic)] Definition kats := Type. End M. Check M.zed@{_}. Fail Check zed. |