Fixing #4887 (confusion between using and with in documentation of firstorder).

1 files changed, 12 insertions, 11 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fa595d915..5eb8cedd9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4343,22 +4343,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder
 
    Tries to solve the goal with {\tac} when no logical rule may apply.
 
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
-   \tacindex{firstorder with}
-
-   Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
-   environment.
-
  \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
    \tacindex{firstorder using}
 
-   Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
-   to the proof-search environment. If {\qualid}$_i$ refers to an inductive
-   type, it is the collection of its constructors which is added as hints.
+   Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search
+   environment. If {\qualid}$_i$ refers to an inductive type, it is
+   the collection of its constructors which are added to the
+   proof-search environment.
 
-\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder with}
 
-  This combines the effects of the {\tt using} and {\tt with} options.
+   Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$
+   to the proof-search environment.
+
+\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the different variants of \texttt{firstorder}.
 
 \end{Variants}