diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-02-05 22:54:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-02-05 22:54:50 +0000 |
| commit | 278498ced8fe68c37007d6d71cf539f3d3d3c0d2 (patch) | |
| tree | 09344a94fe06e300922c1bbb48172cb657749e81 | |
| parent | 8acc26a911f5ad3264c5e83771048f3a3be07ea4 (diff) | |
Updated.
| -rw-r--r-- | BUGS | 21 | ||||
| -rw-r--r-- | ChangeLog | 57 |
2 files changed, 75 insertions, 3 deletions
@@ -1,9 +1,22 @@ -*- outline -*- -* Bugs to be fixed before PG 3.5 is released. +* Bugs to be fixed before PG 3.5 is released; recently noted items -The items below are known and will be fixed before 3.5 is released. -Please don't send email about them (unless you can fix them). +The items below are known and will be fixed (or shifted to the list +below) before 3.5 is released. Please don't send email about them +(unless you can fix them). + +** Various menu problems with Emacs 21.2. + +PG menus may be added to wrong bar during autoload. See CHANGES for +temporary workaround. + + +** Occasional appearance of <^sync> messages in Isabelle/Isar output + +Due to a patch for Coq that has changed some internals. Patch is due +to be reverted, Coq itself has been changed to avoid need for the +hack. May cause other glitches with Isabelle. ** UTF-8 problems with Red Hat 8.0 / glibc 2.2 and (at least) Coq. @@ -28,8 +41,10 @@ be read the shell. This will affect all applications, though. + ================================================================= + * Known Bugs and Workarounds for Proof General. Contact: mailto:bugs@proofgeneral.org @@ -1,3 +1,60 @@ +2003-02-05 David Aspinall <da@proofgeneral.org> + + * etc/ProofGeneral.spec, generic/proof-site.el, html/develdownload.php, html/devel.html: + Set version tag for new release. + + * CHANGES: Updated. + + * generic/proof-config.el: + Doc generalisation of proof-script-command-end-regexp. + + * generic/proof-script.el: + Tweak proof-script-generic-parse-cmdend to allow .. fix for Coq parsing + + * etc/coq/parsingdot.v: New files. + + * coq/coq.el: + New setting for parse cmdend regexp. + + * generic/proof-menu.el: + Compatibility function for customize-menu-create + + * generic/proof-compat.el: + Give up on customize-menu-create on GNU Emacs + +2003-02-05 Pierre Courtieu <courtieu@lri.fr> + + * doc/ProofGeneral.texi: + Added a paragraph in the documentation for the variable coq-version-is-V74. + +2003-02-04 Pierre Courtieu <courtieu@lri.fr> + + * coq/coq-syntax.el: + Coq/pg: fixed a little bug with the "Print Hint" state preserving + command, which must not be matched by the state changing command + "Hint". I put "\\`Hint" in the keyword list, but I am not sure this is + the best way. + +2003-02-03 David Aspinall <da@proofgeneral.org> + + * ChangeLog: Updated. + + * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: + Set version tag for new release. + +2003-02-03 Pierre Courtieu <courtieu@lri.fr> + + * coq/coq.el, coq/coq-syntax.el, coq/example.v, coq/ex-module.v: + code cleaning + deals better with the new module system of Coq. Did + not test the fsfemacs. Will do before release. + +2003-02-03 sberghof <sberghof@dcs.ed.ac.uk> + + * isar/isar.el: + - Moved "show me" menu one level up in the menu hierarchy + - Reordered entries in "show me" menu and added entry for displaying matching + introduction rules + 2003-02-03 David Aspinall <da@proofgeneral.org> * etc/ProofGeneral.spec, html/develdownload.php, html/devel.html, generic/proof-site.el: |