diff options
Diffstat (limited to 'generic/proof-useropts.el')
| -rw-r--r-- | generic/proof-useropts.el | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 4ce51c99..1432776f 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -99,6 +99,21 @@ be inserted as the user types commands to the prover." :set 'proof-set-value :group 'proof-user-options) +(defcustom proof-omit-proofs-option nil + "Set to t to omit complete opaque proofs for speed reasons. +When t, complete opaque proofs in the asserted region are not +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. + +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) + (defcustom pg-show-hints t "*Whether to display keyboard hints in the minibuffer." :type 'boolean |