diff options
| -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. |