From f7943ba646c258a0a4a5b397b8a920d5d13ecf31 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Wed, 17 Mar 2021 08:37:38 +0100
Subject: prefix arg for temporarily disabling omitting proofs

Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.
---
 doc/ProofGeneral.texi | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index beb5cc9f..49275d64 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1522,15 +1522,19 @@ deleted text.
 
 
 @c TEXI DOCSTRING MAGIC: proof-goto-point
-@deffn Command proof-goto-point 
+@deffn Command proof-goto-point &optional raw
 Assert or retract to the command at current position.@*
 Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as
-appropriate.
+appropriate. With prefix argument @var{raw} the omit proofs feature
+(@samp{@code{proof-omit-proofs-option}}) is temporaily disabled to check all
+proofs in the asserted region.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-process-buffer
-@deffn Command proof-process-buffer 
-Process the current (or script) buffer, and maybe move point to the end.
+@deffn Command proof-process-buffer &optional raw
+Process the current (or script) buffer, and maybe move point to the end.@*
+With prefix argument @var{raw} the omit proofs feature (@samp{@code{proof-omit-proofs-option}})
+is temporaily disabled to check all proofs in the asserted region.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-retract-buffer
-- 
cgit v1.2.3