Merge PR #932: Fix shuffled documentation.

1 files changed, 7 insertions, 7 deletions

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index b93ca29577..1609e4a041 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -51,6 +51,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
@@ -86,13 +92,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}