diff options
Diffstat (limited to 'BUGS')
-rw-r--r-- | BUGS | 43 |
1 files changed, 43 insertions, 0 deletions
@@ -36,3 +36,46 @@ allocation. Maybe some of the spans aren't removed properly. Setting a limit on the size of the process buffer doesn't seem to help. (1998/10/06: Is this bug still present? Test examples?) +*`proof-zap-commas-region' does not work for Emacs 20.2 on + lego/example.l . On *initially* fontifying the buffer, + commas are not zapped. However, when entering text, commata are + zapped correctly. Workaround: don't stare too much at commata + +*`proof-find-next-terminator' (bound to C-c C-e) doesn't work +properly. Workaround: use other means to navigate in a proof scipt +buffer. + + +LEGO Proof General Bugs +======================= + +* A thorny issues are local definitions in a proof state. LEGO cannot +undo them explicitly. Workaround: retract back to a command before a +definition. + +* Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone +in a proof state by the Proof General. Workaround: retract back to the +start of the proof. + +* After LEGO has issued a `*** QED ***' you may undo steps in the proof +as long as you don't issue a `Save' command or start a new proof. The +LEGO Proof General assumes that all proofs are terminated with a +proper `Save' command. Workaround: Always issue a `Save' command after +completing a proof. If you forget one, you should retract to a point +before the offending proof development. + +*legotags doesn't find all declarations. It cannot handle lists e.g., +with [x,y:nat]; it only tags x but not y. [The same problem exists for +coqtags] Workaround: don't rely too much on the etags mechanism. + +Coq Proof General Bugs +====================== + +*coqtags doesn't find all declarations. 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. + |