diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-04 19:34:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-04 19:36:09 +0100 |
| commit | dc4200a1c0e37a600537fd1809377a3137ce0cc3 (patch) | |
| tree | 69ecf19bc376ec2fddb95f9eb89529027ed73591 /pretyping | |
| 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 'pretyping')
0 files changed, 0 insertions, 0 deletions