diff options
| author | Hendrik Tews | 2021-03-25 23:02:32 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-16 22:53:05 +0200 |
| commit | 560c6a27d0f082c596284d133fc8af4bc89a6f15 (patch) | |
| tree | 11de5c87a2b4a8001479de7babaae9a57d217a95 /doc/ProofGeneral.texi | |
| parent | 05399b7129a77efcfa7f63d8112474cdab9398e0 (diff) | |
omit proofs: emit warning on nested proofs and continue
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index c8f0c4c7..43f3ccb0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -5221,6 +5221,10 @@ With a prefix argument, both @code{proof-goto-point} and @code{proof-process-buffer} will temporarily disable the omit proofs feature and send the full proof script to Coq. +If a nested proof is detected while searching for opaque proofs +to omit, a warning is displayed and the complete remainder of the +asserted region is sent unmodified to Coq. + @node Editing multiple proofs @section Editing multiple proofs |