diff options
| author | Pierre-Marie Pédrot | 2016-05-02 11:17:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-02 11:18:25 +0200 |
| commit | 9462ef0ad6eb233c2f74bb400a262ddefd880386 (patch) | |
| tree | 00bb8466401391de37a5c9b25e90b7413cc86bc4 /dev | |
| parent | 97adfc372fd716c6701677b69950cd9279f46f27 (diff) | |
Generate parsing rules for ML tactics in the same order as before a7917a32.
Once again showing the fragility of the parsing engine, commit a7917a32
reversed the relative order of the declaration of parsing rules for tactics
declared through TACTIC EXTEND. There is probably no good order at all, but
for retrocompatibility, this patch enforces the original one.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions