diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /test-suite/success/Notations2.v | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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. |