diff options
| author | Hendrik Tews | 2021-03-17 08:37:38 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-16 22:53:05 +0200 |
| commit | f7943ba646c258a0a4a5b397b8a920d5d13ecf31 (patch) | |
| tree | 26647718255a8a6f04f51123fe9e67ec0255603a /generic/proof-useropts.el | |
| parent | e454ae013827b98b814c99ffbc1ca7f2525fb030 (diff) | |
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.
Diffstat (limited to 'generic/proof-useropts.el')
| -rw-r--r-- | generic/proof-useropts.el | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index d5df0404..1432776f 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -106,7 +106,11 @@ sent to the proof assistant (and thus not checked). For files with big proofs this can drastically reduce the processing time for the asserted region at the cost of not checking the proofs. For partial and non-opaque proofs in the asserted region all -proof commands are sent to the proof assistant." +proof commands are sent to the proof assistant. + +Using a prefix argument for `proof-goto-point' (\\[proof-goto-point]) +or `proof-process-buffer' (\\[proof-process-buffer]) temporarily +disables omitting proofs." :type 'boolean :group 'proof-user-options) |