Added changes in CHANGE about my new customization variables

coq-user-backable-command etc.

1 files changed, 45 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 931d721c..1480a7a4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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