diff options
| author | Hugo Herbelin | 2019-10-06 14:33:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-31 15:31:55 +0100 |
| commit | 6363875a682ffa36f1f80fa74314c0b68cb2f065 (patch) | |
| tree | 8a6f4adbbb00a26dc2f51583319cb3f1145f90f1 /kernel | |
| parent | 23462f128c08922d93e11d65fffb5dca6691639c (diff) | |
More tolerant in format for recursive notations.
This is probably a bit overkill but users are tempted to experiment
it, so we accept that both ends of a recursive notation are surrounded
with boxes which contain printing hints.
The alternative would have been to forbid the ends of a recursive
notation to be in boxes, but strictly speaking it is a bit more
restricting, even if I don't see a realistic use of the general form.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions