diff options
| -rw-r--r-- | test-suite/success/Notations2.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 7c2cf3ee52..d01ebfb18e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -126,3 +126,11 @@ 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. |