| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
|
| |
|
|
| |
The two previous commits make the warning irrelevant and useless.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
Supporting accordingly printing of sequences of binders including binding
patterns.
|
| | |
|
| |
|
|
|
|
|
| |
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
|
| |
|
|
| |
immediately in the scope of another recursive pattern.
|
| | |
|
| |
|
Paul Steckler
Hugo Herbelin
Pierre-Marie Pédrot