diff options
author | 2017-07-28 14:54:46 +0200 | |
---|---|---|
committer | 2017-07-28 14:54:46 +0200 | |
commit | a35d5b4aa252a2f18691a44eb33945271aed496a (patch) | |
tree | e628b3cc44b551096435b208926baf34ab3c1564 | |
parent | 2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (diff) |
Fix shuffled documentation.
-rw-r--r-- | doc/refman/AsyncProofs.tex | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7ffe25225..5a3b90f04 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -46,6 +46,12 @@ proof does not begin with \texttt{Proof using}, the system records in an auxiliary file, produced along with the \texttt{.vo} file, the list of section variables used. +\subsubsection{Automatic suggestion of proof annotations} + +The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a +\texttt{Qed} command is processed, a correct proof annotation. It is up +to the user to modify the proof script accordingly. + \section{Proof blocks and error resilience} Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq @@ -81,13 +87,7 @@ CoqIDE one of the following options: \texttt{-async-proofs-tactic-error-resilience off}, \texttt{-async-proofs-tactic-error-resilience all}, \texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. -Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. - -\subsubsection{Automatic suggestion of proof annotations} - -The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a -\texttt{Qed} command is processed, a correct proof annotation. It is up -to the user to modify the proof script accordingly. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. \section{Interactive mode} |