| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
|
|
|
| |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| |
|
|
|
|
|
|
|
| |
Since camlp5 parses from left, the last ", z" was parsed as part of an
arbitrary long list of "x1 , .. , xn" and a syntax error was raised
since an extra ", z" was still expected.
We support this by translating "x , .. , y , z" into "x , y , .. , z"
and reassembling the arguments appropriately after parsing.
|
| | |
|
| |
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Pierre-Marie Pédrot
Matej Kosik