diff options
| author | Hugo Herbelin | 2019-12-25 13:57:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-15 22:23:08 +0100 |
| commit | 44ec3c8fd02f27d1dc7123bfbe5f5018937d6b86 (patch) | |
| tree | df70757eab8071ae32ef97581e752dddf7637493 /test-suite/output | |
| parent | d122f7d5ffd5d3b26153a0ad7b74a669b8dd1c9d (diff) | |
Fixes #11331 (unexpected level collisions between custom entries and constr).
There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).
Also fixes #9517, fixes #9519, fixes #9640 (part 3).
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations4.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 8 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f65696e464..807914a671 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -71,3 +71,7 @@ The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". The command has indeed failed with message: The format is not the same on the right- and left-hand sides of the special token "..". +Entry constr:expr is +[ "201" RIGHTA + [ "{"; constr:operconstr LEVEL "200"; "}" ] ] + diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4de6ce19b4..2906698386 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -184,3 +184,11 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). End M. + +Module Bug11331. + +Declare Custom Entry expr. +Notation "{ p }" := (p) (in custom expr at level 201, p constr). +Print Custom Grammar expr. + +End Bug11331. |