From 29fa6d27c20493a472045c5fb4c5a442cfdcfac7 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 7 Sep 2006 17:39:36 +0000 Subject: Updated CHANGES. --- coq/CHANGES | 66 +------------------------------------------------------------ 1 file changed, 1 insertion(+), 65 deletions(-) (limited to 'coq') diff --git a/coq/CHANGES b/coq/CHANGES index 83a21b97..d5e8ab68 100644 --- a/coq/CHANGES +++ b/coq/CHANGES @@ -2,68 +2,4 @@ * Summary of Changes for coq / Proof General 3.6 -*** No more support for coq 7.x - -*** Much better PG/Coq synchronizing system for coq >= 8.1 - - Synchronization is not based on script parsing anymore, which - makes it much more reliable. - - In particular you don't need to set - coq-user-state-changing-commands and others anymore (was needed - for your own tactics/commands). See next point. - - Coq v8.0 is still supported, if for some reason PG does not see - that your coq version is a 8.0 (read *Message* after loading a .v - file), then set variable coq-version-is-V8-0 to t in your emacs - init file. Otherwise PG will hang at first line when scripting. - -*** New variables coq-user-commands-db and coq-user-tactics-db - - User defined tactics/commands information. See C-h v coq-syntax-db - for syntax. It is not necessary to add your own tactics here (it is - not needed by the synchronizing/backtracking system). You may - however do so for the following reasons: - - 1 your tactics/commands will be colorized by font-lock - - 2 your tactics/commands will be added to the menu and to completion - when calling coq-insert-tactic/command (see below) - - 3 you may define an abbreviation for your tactic/command. - -*** Much better indentation - - More robust. nested comments are OK even in xemacs. Still a bit - slow on big files. - - indent-region won't touch comments, but indenting comments with - tab (indent-according-to-mode) will. - -*** Better font-lock coloration - -*** new coq-insert-tactic and coq-insert-command function - - These two functions allow to insert a tactic or command with - completion in the mini-buffer. - -*** Local Variables List semi automatic filling - - Local Variables Lists are used to set coq program name and arguments - persistently for a given file. The menu entry "set coq prog - persistently" helps you to define or change the values in this list - (which are store as a comment at the end of the file, see info - manual at node ((emacs)File Variables). - -*** automatic insertion of "match...with" for a given type - - This coqide great feature has been added. - -*** error highlighting - - When scripting, error with location information are parsed and the - corresponding part of the scripting buffer is highlighted. Also - inpsired from coqide. - -*** new "queries" menu - +moved to ../CHANGES \ No newline at end of file -- cgit v1.2.3