diff options
| author | Guillaume Melquiond | 2016-04-28 20:38:07 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-04-28 20:38:07 +0200 |
| commit | 5bcccd7ed80acdb9904d5a623f1aba42183803a4 (patch) | |
| tree | 64467789bbd35dea0490b25e3d44fc58cc7e2b1a /pretyping | |
| parent | 1aa989f13a3d3a3171dd09e4727394b88bc4b8ce (diff) | |
Make the language grammar much more precise. (Fix bugs #4682 and #4683)
Rather than being isolated words, commands and tactics now extend till
dot separators. So bullets can be defined as living only at the top level
of proofs, which should make their detection much more robust.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions