diff options
| author | Erik Martin-Dorel | 2021-04-21 20:00:36 +0200 |
|---|---|---|
| committer | GitHub | 2021-04-21 20:00:36 +0200 |
| commit | b5c4c3a1423c7925194334d66c262054d6a6c4c5 (patch) | |
| tree | e7878c97ece66bd7941e8f6019f70325de3f1bd1 /generic/proof-useropts.el | |
| parent | d0acb626eba17023c55b002921870d60e48527a5 (diff) | |
| parent | 82311da10ee3dfa6f29ddfb9225f9f05c29dca31 (diff) | |
Add feature to omit complete opaque proofs
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 |