diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:12:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:12:20 +0200 |
| commit | a82c30c08c7442b6bb43829d2be6a299f493ca88 (patch) | |
| tree | fc4ee6e5e395c94d15d2b7109ee00c7372b5a31d /CHANGES | |
| parent | c3f7302e9f6849298bbb34dc91516751444888ff (diff) | |
| parent | f1531b5deb0f2bbb5653bb6f02abf6a1896f399a (diff) | |
Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -5,6 +5,8 @@ Notations - Recursive notations with the recursive pattern repeating on the right (e.g. "( x ; .. ; y ; z )") now supported. +- Notations with a specific level for the leftmost nonterminal, + when printing-only, are supported. Tactics |