diff options
| -rw-r--r-- | CHANGES | 13 | ||||
| -rw-r--r-- | etc/announce | 8 | ||||
| -rw-r--r-- | etc/release-log.txt | 4 | ||||
| -rw-r--r-- | todo | 9 |
4 files changed, 28 insertions, 6 deletions
@@ -2,6 +2,8 @@ * Summary of Changes for Proof General 3.5 from 3.4 +See also etc/release-log.txt for minor patches. + ** Generic changes *** Support for Speedbar and Index menu ("Imenu") @@ -237,9 +239,17 @@ than using Elisp. ** Changes for Coq +*** Coq 8.0 compatibility. Example files are Coq 8.0 format. + +**** Possibility to run Coq 8.0 in compatibility mode +**** Further prover settings added +**** Automatic compilation ("auto-compile-vos"), dependencies managed + +*** Command coq-intros inserts intros using "Show Intros" output + *** Indentation improved -*** Menu entries for commands, tactics and terms +*** Menu entries for inserting commands, tactics and terms *** "Holes" system, for editing structured expressions @@ -261,7 +271,6 @@ will be asked if you want to save abbrevs, answer yes. *** X-symbols are much improved (more symbols, cleaner grammar) Much more symbols are supported now (C-= C-= for the symbol table). -See coq/README for the syntax of sub/superscripts. ** Additional instances of Proof General diff --git a/etc/announce b/etc/announce index 811b48c7..1b9c0935 100644 --- a/etc/announce +++ b/etc/announce @@ -1,8 +1,8 @@ Announcing Proof General Version 3.5 A Generic Emacs interface for Interactive Proof Assistants - http://proofgeneral.inf.ed.ac.uk + http://proofgeneral.inf.ed.ac.uk - Contact: David Aspinall <da+pg-feedback@inf.ed.ac.uk> + Contact: David Aspinall <da+pg-feedback@inf.ed.ac.uk> Proof General is a generic (X)Emacs interface for proof assistants. It can be instantiated for the proof assistant of your choice, and is @@ -29,8 +29,8 @@ Summary of interesting changes since 3.4: . Keyboard hints and other messages displayed in minibuffer . Auxiliary modes bundled: X-Symbol and MMM Mode . Improved menus, user options, script colouring and active highlighting -. For Coq: a new "holes" system, for editing structured expressions -. For Isabelle: browsing/highlighting theorem dependencies +. For Coq (8.0): extensive templates, automatic compilation support +. For Isabelle (2004): browsing/highlighting theorem dependencies . New instances of PG: Casl Consistency Checker, Shell Script . Additional sample proofs (some from http://www.cs.kun.nl/~freek/comparison/) . Many other minor improvements and editing features diff --git a/etc/release-log.txt b/etc/release-log.txt index ec99be5a..60a27a41 100644 --- a/etc/release-log.txt +++ b/etc/release-log.txt @@ -1,3 +1,7 @@ +XX.04.04 3.5.1 Release forthcoming for improved Coq 8.0 support + +-------------------- + 18.04.04 3.5 Release 3-4 based on branch 8.0 (repeated: 18.04.04 fixes to display handling 21.04.04 modify CHANGES; Coq menu) @@ -5,6 +5,15 @@ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. ================================================================= +3.5.1 Coq-8 fixup release TODO + +* Fix display of sub/super scripts in Coq output +* Multiple file handling +* Automatic adjustment of line width + + +================================================================= + * Developers' Infeasibly Long Low-Level List of Things to Do |