Extending the doc with a general summary of auto variants.

This way of giving the summary avoids redundancy as much as possible.
It is helpful for the auto-completion of Company-Coq of @cpitclaudel.

1 files changed, 25 insertions, 5 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dccd6f590..49a5b7983 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3472,7 +3472,7 @@ hints of the database named {\tt core}.
   Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
   the database {\tt core}. See Section~\ref{Hints-databases} for the
   list of pre-defined databases and the way to create or extend a
-  database.  This option can be combined with the previous one.
+  database.
 
 \item {\tt auto with *}
 
@@ -3486,16 +3486,18 @@ hints of the database named {\tt core}.
   $lemma_i$ is an inductive type, it is the collection of its
   constructors which is added as hints.
 
-\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$
-
-  This combines the effects of the {\tt using} and {\tt with} options.
-
 \item {\tt info\_auto}
 
   Behaves like {\tt auto} but shows the tactics it uses to solve the goal.
   This variant is very useful for getting a better understanding of automation,
   or to know what lemmas/assumptions were used.
 
+\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  This is the most general form, combining the various options.
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and
@@ -3506,6 +3508,14 @@ hints of the database named {\tt core}.
 
 \item \texttt{trivial with *}
 
+\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
+
+\item {\tt info\_trivial}
+
+\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
 \end{Variants}
 
 \Rem {\tt auto} either solves completely the goal or else leaves it
@@ -3537,6 +3547,16 @@ Abort.
 
 Note that {\tt ex\_intro} should be declared as a hint.
 
+\begin{Variants}
+
+\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$
+  {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with}
+  \ident$_1$ {\ldots} \ident$_n$}
+
+  The various options for eauto are the same as for auto.
+
+\end{Variants}
+
 \SeeAlso Section~\ref{Hints-databases}
 
 \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$}