diff options
| -rw-r--r-- | CHANGES | 45 |
1 files changed, 45 insertions, 0 deletions
@@ -66,6 +66,51 @@ Support next error function. Isabelle classic mode: add highlighting improvements for ML code 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. + + coq-user-non-backable-commands: example: "Print" + + coq-user-backable-commands: example: "Require" + + coq-user-undoable-tactics: example: "Intro" + + 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. + +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. + +*** Bug fixed: Better synchronization of PG/Coq. Commands like Hint, +Require, etc, were not backtracked correctly. See the following: + +**** Bug: Unknown commands are not well backtracked +**** Work-around: use the elisp variables cited above. + +**** 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 |