From 535d91629926249c335a17eddae24e1676c0cca0 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 11 Jun 2002 20:33:55 +0000 Subject: CHANGE is cleaner in the Coq part! Not important. --- CHANGES | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/CHANGES b/CHANGES index 1480a7a4..26ce4c4c 100644 --- a/CHANGES +++ b/CHANGES @@ -69,34 +69,35 @@ 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. Tactics and commands -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. + user to register his own tactics and commands. Tactics and + commands 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. - coq-user-non-backable-commands: example: "Print" + coq-user-non-backable-commands: example: "Print" - coq-user-backable-commands: example: "Require" + coq-user-backable-commands: example: "Require" - coq-user-undoable-tactics: example: "Intro" + coq-user-undoable-tactics: example: "Intro" - coq-user-non-undoable-tactics: example: "Proof" + coq-user-non-undoable-tactics: example: "Proof" -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. + 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. -Example: -(setq coq-user-backable-commands '("MyHint" "MyRequire")) + Example: + (setq coq-user-backable-commands '("MyHint" "MyRequire")) -This allows PG to - 1) colorize correctly - 2) more important to correctly backtrack user-defined commands, see - the following paragraphs below on this subject. + This allows PG to + 1) colorize correctly + 2) more important to correctly backtrack user-defined commands, + see the following paragraphs below on this subject. *** Bug fixed: Better synchronization of PG/Coq. Commands like Hint, -Require, etc, were not backtracked correctly. See the following: + Require, etc, were not backtracked correctly. See the following: **** Bug: Unknown commands are not well backtracked **** Work-around: use the elisp variables cited above. -- cgit v1.2.3