diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Notations2.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index aa439fae12..b26e725d9b 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -172,3 +172,16 @@ Notation "#" := 0 (only printing). Print Visibility. End Bug10750. + +Module M18. + + Module A. + Module B. + Infix "+++" := Nat.add (at level 70). + End B. + End A. +Import A. +(* Check that the notation in module B is not visible *) +Infix "+++" := Nat.add (at level 80). + +End M18. |