From dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Sep 2009 13:24:21 +0000
Subject: - 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
---
 doc/refman/RefMan-tac.tex | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3