diff options
| author | Vadim Zaliva | 2019-12-04 16:01:58 -0800 |
|---|---|---|
| committer | GitHub | 2019-12-04 16:01:58 -0800 |
| commit | a920a00ba9dd1a5e5f21cd03c6c565ebb600ffab (patch) | |
| tree | 43042beef7eb7e95bb04c8184f1470f6f7ee3754 /doc | |
| parent | 15ccaec24ce935de366cae08b906c130379758ce (diff) | |
Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions