diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-09-09 16:57:55 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-09-09 16:57:55 +0000 |
| commit | 4ae205b8cd8dd8f0b5f8ac8308e63246733e70fd (patch) | |
| tree | 652cd5ff177145efd14178b27909ec90b5ddf467 /coq | |
| parent | 4ae05c6d7ea170c101df8ec8c3b56b412477b9f9 (diff) | |
Bug in new parsing for coq, mention
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/BUGS | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -4,6 +4,12 @@ See also ../BUGS for generic bugs. +** With new syntax in Coq 7, comments at end of files cannot be processed. + +Leads to annoying retract/process questions when switching buffers. +Workaround: don't use a comment as the last line of the buffer, for now. + + ** coqtags doesn't find all declarations. It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x |