diff options
| author | Hugo Herbelin | 2020-02-22 01:43:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 08:35:59 +0100 |
| commit | 2e64c61cf64172fb0dce2d8b3996fb30e179e5ea (patch) | |
| tree | 7d585e0649430fd564ada3e4b0445c2be2e387c2 /test-suite | |
| parent | 1d840bf16744717e3289afaf66db4c44a7f7d814 (diff) | |
Fixing a bug introduced in PR #10832 (new format specific to a given notation).
The import of the format should not be done if i<>1 in open_notation.
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. |