From 4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 27 Sep 2016 15:21:37 +0200
Subject: Fixing #4887 (confusion between using and with in documentation of
 firstorder).

---
 doc/refman/RefMan-tac.tex | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fa595d9159..5eb8cedd95 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}
 
-- 
cgit v1.2.3