diff options
| author | David Aspinall | 2002-08-12 14:31:37 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-08-12 14:31:37 +0000 |
| commit | 614d64d46e0e8a3c6fa1d67ec04fd2e442cdb267 (patch) | |
| tree | 3dd413c61308d8fc5c13d253ba3ad58b354c2b4d | |
| parent | a01e26ea4f1f8268b767ed7604aa561d7f2b2fa2 (diff) | |
Tweak Pierres docs
| -rw-r--r-- | doc/ProofGeneral.texi | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index a2c55c3c..d36f6cf0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3278,9 +3278,11 @@ whitespaces". See the Emacs documentation of @code{regexp-quote} for the syntax and semantics. WARNING: you need to restart Emacs to make the changes to these variables effective. -In case of losing synchronization, the user can use @kbd{C-c C-z} +In case of losing synchronization, the user can use @kbd{C-c C-z} to +move the locked region to the proper position, (@code{proof-frob-locked-end}, @pxref{Escaping script management}) or -@kbd{C-c C-v} to re-issue an erroneously back-tracked tactic. +@kbd{C-c C-v} to re-issue an erroneously back-tracked tactic without +recording it in the script. @c |