diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2002-07-26 19:42:18 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2002-07-26 19:42:18 +0000 |
| commit | 325784e32122802b42aff7254423db0ca9509fb4 (patch) | |
| tree | 2a6a715b5a95207022781427f9ba0363852157c0 /doc | |
| parent | 819d64f05308713f1e3a46b8d7b3baa74c896f43 (diff) | |
Changed a bit more the doc and the CHANGES file, to be
consitent. Concerns the coq-user... variables.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 14 |
1 files changed, 7 insertions, 7 deletions
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 |