diff options
Diffstat (limited to 'test-suite/success/Notations2.v')
-rw-r--r-- | test-suite/success/Notations2.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 7c2cf3ee..1b33863e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -126,3 +126,31 @@ Notation "'myexists' x , p" := (ex (fun x => p)) (at level 200, x ident, p at level 200, right associativity) : type_scope. Check myexists I, I = 0. (* Should not be seen as a constructor *) End M14. + +(* 15. Testing different ways to give the same levels without failing *) + +Module M15. + Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level). + Fail Local Notation "###### x" := (S x) (right associativity, at level 79). + Local Notation "###### x" := (S x) (at level 79). +End M15. + +(* 16. Some test about custom entries *) +Module M16. + (* Test locality *) + Local Declare Custom Entry foo. + Fail Notation "#" := 0 (in custom foo). (* Should be local *) + Local Notation "#" := 0 (in custom foo). + + (* Test import *) + Module A. + Declare Custom Entry foo2. + End A. + Fail Notation "##" := 0 (in custom foo2). + Import A. + Local Notation "##" := 0 (in custom foo2). + + (* Test Print Grammar *) + Print Grammar foo. + Print Grammar foo2. +End M16. |