diff options
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 12 |
1 files changed, 8 insertions, 4 deletions
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 |