diff options
| author | David Aspinall | 2002-09-11 14:47:28 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-09-11 14:47:28 +0000 |
| commit | 0d3342242b9a327331da0f71e667a0afe206430b (patch) | |
| tree | ad66c68c7ed5e83107124a6f0e5a367c6e07e010 /coq | |
| parent | 49847430fd13427d589d909b8d083cb1d830055e (diff) | |
Updated.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/BUGS | 10 |
1 files changed, 1 insertions, 9 deletions
@@ -4,10 +4,6 @@ See also ../BUGS for generic bugs. -** X-Symbol does not work on GNU Emacs. - -Please don't even try it, it will mess up your Emacs. - ** With new syntax in Coq 7, comments at end of files cannot be processed. Leads to annoying retract/process questions when switching buffers. @@ -19,11 +15,7 @@ It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x but not y. [The same problem exists for legotags] Workaround: don't rely too much on the etags mechanism. -** User defined tactics cannot be retracted. - - Workaround: you may need to retract to the beginning of the proof. - -** Coq Proof General does not know about Coq's Section mechanism. +** With Coq 7, multiple file handling and auto-compilation is buggy ** Surely others that aren't mentioned here... |