diff options
Diffstat (limited to 'doc')
| -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 |