diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | coq/BUGS | 10 |
2 files changed, 4 insertions, 9 deletions
@@ -15,7 +15,10 @@ ** Generic changes +*** Display management: added shring-windows-tofit option +Attempt to shrink output windows to fit their contents in +case it is less than 1/2 the window height. In progress. *** Parsing internals changed: minor user visible differences @@ -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... |