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

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

2 files changed, 39 insertions, 20 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
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 65e41ecb..4f3a5f7a 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3209,20 +3209,20 @@ We give an example of existing commands that fit each category.
 
 @item @code{coq-user-state-preserving-commands}: example: "@code{Print}"
 
-@item @code{coq-user-backable-commands}: example: "@code{Require}"
+@item @code{coq-user-state-changing-commands}: example: "@code{Require}"
 
-@item @code{coq-user-undoable-tactics}: example: "@code{Intro}"
+@item @code{coq-user-state-changing-tactics}: example: "@code{Intro}"
  
-@item @code{coq-user-non-undoable-tactics}: example: "@code{Idtac}"
+@item @code{coq-user-state-preserving-tactics}: example: "@code{Idtac}"
 @end itemize
 
-This variables are string lists. See their documentations in emacs
-(@code{C-h v coq-user...})  for details on how to set them in your .emacs
-file. The strings can contain some escaped regexp feature.
+This variables regexp string lists. See their documentations in emacs
+(@code{C-h v coq-user...})  for details on how to set them in your
+.emacs file.
 
 Example:
 @lisp
-(setq coq-user-backable-commands 
+(setq coq-user-state-changing-commands 
       '("MyHint" "MyRequire" "Show\\s-+Mydata"))
 @end lisp