diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/attribute-syntax.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v index 83fb3d0c8e..241d4eb200 100644 --- a/test-suite/success/attribute-syntax.v +++ b/test-suite/success/attribute-syntax.v @@ -1,4 +1,4 @@ -From Coq Require Program. +From Coq Require Program.Wf. Section Scope. @@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _. #[deprecated(since="8.9.0")] Ltac foo := foo. + +Module M. + #[local] #[polymorphic] Definition zed := Type. + + #[local, polymorphic] Definition kats := Type. +End M. +Check M.zed@{_}. +Fail Check zed. +Check M.kats@{_}. +Fail Check kats. |