diff options
| author | Hugo Herbelin | 2016-11-04 19:34:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-11-04 19:36:09 +0100 |
| commit | dc4200a1c0e37a600537fd1809377a3137ce0cc3 (patch) | |
| tree | 69ecf19bc376ec2fddb95f9eb89529027ed73591 /plugins/syntax | |
| parent | 94bdd90bacc4d4a92b79bbe0db532e523fbcbce8 (diff) | |
Quick fix of tactic parsing while Load-ing in coqide.
Note that this is still broken when loading files containing C-zar scripts.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions