From 614d64d46e0e8a3c6fa1d67ec04fd2e442cdb267 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 12 Aug 2002 14:31:37 +0000
Subject: Tweak Pierres docs

---
 doc/ProofGeneral.texi | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3