Changed a bit more the doc and the CHANGES file, to be

consitent. Concerns the coq-user... variables.

1 files changed, 32 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 06a66c79..960aae1b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,24 +73,43 @@ Commands like Hint, Require, etc, were not backtracked correctly, but
 are now. Nested proofs and commands nested in proofs are now also well
 backtracked.
 
-User defined keywords are not completely well backtracked. To solve
-this we provide customization, using four configurable variables for
-registering personal tactics and commands. Commands and tactics are
-split into backable (resp. undoable), i.e. which need "Back"
-(resp. "Undo") to be backtracked and not backable (resp. not
-undoable). This allows PG to 1) colorize correctly 2) (more important)
-to correctly backtrack user-defined commands and tactics.
-
-See `coq-user-non-backable-commands', `coq-user-backable-commands',
-`coq-user-undoable-tactics', `coq-user-non-undoable-tactics'
+User defined keywords could not completely well backtracked. The
+fall-back mechanism is better now, but to solve this completely we
+provide four configurable variables for registering personal tactics
+and commands. Commands and tactics are split into state-preserving or
+state-changing commands and tactics, i.e. which need or not Back/Undo
+to be backtracked. This allows PG to
+1) (more important) to correctly backtrack user-defined commands and
+   tactics.
+2) colorize correctly 
+
+See `coq-user-state-preserving-commands, `coq-user-state-changing-commands,
+`coq-user-state-preserving-tactics, `coq-user-state-changing-tactics'
 
 These variables are regexp lists. See their documentations in emacs of
-this variable (C-h v coq-user...)  for details on how to set them in
-your .emacs file.   Example:
+this variable (C-h v coq-user...) and in the doc, for details on how
+to set them in your .emacs file.  Example:
+
+ An example of existing commands that fit each category:
+
+   coq-user-state-preserving-commands: example: "Print"
+
+   coq-user-state-changing-commands:     example: "Require"
+
+   coq-user-state-changing-tactics:      example: "Intro"
+
+   coq-user-state-preserving-tactics:  example: "Proof"
+
+   This variables are string lists. See the documentations in emacs of
+   this variable (C-h v coq-user...)  for details on how to set them
+   in your .emacs file.
 
-   (setq coq-user-backable-commands 
+   Example:
+   (setq coq-user-state-changing-commands 
 	  '("MyHint" "MyRequire" "Show\\-+Mydata"))
 
+	Last thing: you must restart emacs to allow emacs take these
+	variable into account.
 
 
 ** Changes for other provers