From 419000a975f371612bb77efe1fdf64305fbc5e51 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 12 Jun 2002 11:18:08 +0000 Subject: Changed the CHANGES file for Coq. --- CHANGES | 55 ++++++++++++++++++++++++------------------------------- 1 file changed, 24 insertions(+), 31 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index a3f47cbe..340cf99f 100644 --- a/CHANGES +++ b/CHANGES @@ -68,49 +68,42 @@ contributed by Lucas Dixon (lucasd@dai.ed.ac.uk) ** Coq Changes -*** New Feature: There are some configurable variables that allow the - user to register his own tactics and commands. commands and - Tactics are split into backable (resp. undoable), i.e. which need - "Back" (resp. "Undo") to be backtracked and not backable - (resp. not undoable). We give an example of existing commands that - fit each category. +*** Bug fixed: Much better synchronization of PG/Coq. Commands like + Hint, Require, etc, were not backtracked correctly. Nested proofs + and commands nested in proofs are now also well backtracked, + provided user defined keywords are introduced in the adequat + custom variables, see new feature below. - coq-user-non-backable-commands: example: "Print" +*** New Feature: four Configurable variables allows to register + personal new tactics and commands. Commands and Tactics are split + into backable (resp. undoable), i.e. which need "Back" + (resp. "Undo") to be backtracked and not backable (resp. not + undoable). - coq-user-backable-commands: example: "Require" + This allows PG to + 1) colorize correctly + 2) (more important) to correctly backtrack user-defined commands + and tactics. - coq-user-undoable-tactics: example: "Intro" - coq-user-non-undoable-tactics: example: "Proof" + We give an example of existing commands that fit each category. - This variables are string lists. See their documentations in emacs - of this variable (C-h v coq-user...) for details on how to set - them. + coq-user-non-backable-commands: example: "Print" - Example: - (setq coq-user-backable-commands '("MyHint" "MyRequire")) + coq-user-backable-commands: example: "Require" + coq-user-undoable-tactics: example: "Intro" - This allows PG to - 1) colorize correctly - 2) more important to correctly backtrack user-defined commands, - see the following paragraphs below on this subject. + coq-user-non-undoable-tactics: example: "Proof" -*** Bug fixed: Better synchronization of PG/Coq. Commands like Hint, - Require, etc, were not backtracked correctly. See the following: + This variables are string lists. See their documentations in emacs + of this variable (C-h v coq-user...) for details on how to set + them in your .emacs file. -**** Bug: Unknown commands are not well backtracked -**** Work-around: use the elisp variables cited above. + Example: + (setq coq-user-backable-commands '("MyHint" "MyRequire")) -**** Bug: Commands nested in proofs are still not well backtracked - once the proof is saved. -**** Work around: only let no-effect commands inside proofs (like - Print, Check, ...). The best is to use C-c C-v to issue them - directly anyway. -**** Bug: proofs nested in proofs are not well backtracked. -**** Work-around: Don't use this feature (with PG you don't need it - anyway!). ** Changes for other provers -- cgit v1.2.3