diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2002-06-11 20:33:55 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2002-06-11 20:33:55 +0000 |
| commit | 535d91629926249c335a17eddae24e1676c0cca0 (patch) | |
| tree | 414d2cad743a978647e06001eb6b9a99c3322b52 /CHANGES | |
| parent | 2796a661a0c57be12fe7310ada6bb7519de23c63 (diff) | |
CHANGE is cleaner in the Coq part! Not important.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 37 |
1 files changed, 19 insertions, 18 deletions
@@ -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. |