- Inductive types in the "using" option of auto/eauto/firstorder are

  interpreted as using the collection of their constructors as hints.
- Add support for both "using" and "with" in "firstorder". Made the
  syntax of "using" compatible with the one of "auto" by separating
  lemmas by commas. Did not fully merge the syntax: auto accepts
  constr while firstorder accepts names (but are constr really useful?).
- Added "Reserved Infix" as a specific shortcut of the corresponding
  "Reserved Notation".



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 6 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index abc294e8b1..6dbdaedd43 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3115,10 +3115,16 @@ hints of the database named {\tt core}.
   Uses all existing hint databases, minus the special database
   {\tt v62}. See Section~\ref{Hints-databases}
 
-\item \texttt{auto using $lemma_1, \ldots, lemma_n$}
+\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$}
 
-  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be combined
-  with the \texttt{with \ident} option).
+  Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to
+  hints (can be combined with the \texttt{with \ident} option). If
+  $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$ , \ldots , \nterm{lemma}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
 
 \item {\tt trivial}\tacindex{trivial}
 
@@ -3300,11 +3306,17 @@ instead may reason about any first-order class inductive definition.
    Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
    environment.
 
- \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }
+ \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
    \tacindex{firstorder using}
 
-   Adds lemmas in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$
-   to the proof-search environment.
+   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.
+
+\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
+
 \end{Variants}
 
 Proof-search is bounded by a depth parameter which can be set by typing the