diff options
| author | Hugo Herbelin | 2018-09-24 23:14:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 9bc339f529fc2ee2389a717914514829a73686bc (patch) | |
| tree | 5ccbfe4c7e6cb1c6c5648830a5f1debda4e19926 /test-suite | |
| parent | 06fc6caa49b67526cf3521d1b5885aae6710358b (diff) | |
Fixing #8551 (missing delimiters when notation exists both lonely and in scope).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 12 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d25ad5dca8..acd69f3f50 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -21,3 +21,5 @@ Let "x" e1 e2 : expr Let "x" e1 e2 : expr +fun x : nat => (# x)%nat + : nat -> nat diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 191a073051..12e98c3d64 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -94,3 +94,15 @@ Coercion App : expr >-> Funclass. Check (Let "x" e1 e2). End D. + +(* Check fix of #8551: a delimiter should be inserted because the + lonely notation hides the scope nat_scope, even though the latter + is open *) + +Module E. + +Notation "# x" := (S x) (at level 20) : nat_scope. +Notation "# x" := (Some x). +Check fun x => (# x)%nat. + +End E. |