MAJ du manuel de référence

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

1 files changed, 37 insertions, 15 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d9e600784..93a7406eb 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -149,6 +149,10 @@ usable in the proof development.
   its body. Otherwise said, this tactic turns a definition into an
   assumption.
 
+\item \texttt{clear - {\ident}.} 
+
+  This tactic clears all hypotheses except the ones depending in {\ident}.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -527,6 +531,10 @@ in the list of subgoals remaining to prove.
   This tactic behaves like \texttt{assert} but tries to apply {\tac}
   to any subgoals generated by \texttt{assert}.
 
+\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
+
+   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
+
 \end{Variants}
 
 % PAS CLAIR;
@@ -1125,6 +1133,11 @@ induction n.
 scheme of name {\qualid}. It does not expect that the type of
 {\term} is inductive.
 
+\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+
+  where {\qualid} is an induction principle with complex predicates
+  (like the ones generated by function induction).
+
 \item {\tt induction {\term} using {\qualid} as {\intropattern}}
 
   This combines {\tt induction {\term} using {\qualid}}
@@ -1308,6 +1321,7 @@ components of an hypothesis.
 An introduction pattern is either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
+\item the pattern \texttt{?}
 \item a variable
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
@@ -1319,6 +1333,8 @@ structure of the pattern given as argument:
 \begin{itemize}
 \item introduction on the wildcard do the introduction and then
   immediately clear (cf~\ref{clear}) the corresponding hypothesis;
+\item introduction on \texttt{?} do the introduction, and let Coq
+  choose a fresh name for the variable;
 \item introduction on a variable behaves like described in~\ref{intro}; 
 \item introduction over a
 list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
@@ -1509,7 +1525,10 @@ implicit type of $t$ and $u$.
 This tactic applies to any goal. The type of {\term}
 must have the form
 
-\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. 
+\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. 
+
+\noindent where \texttt{eq} is the Leibniz equality or a registered
+setoid equality.
 
 \noindent Then {\tt rewrite \term} replaces every occurrence of 
 \term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are
@@ -1536,10 +1555,14 @@ This happens if \term$_1$ does not occur in the goal.
 \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
-\item {\tt rewrite {\term} in {\ident}}
+\item {\tt rewrite {\term} in {\clause}}
   \tacindex{rewrite \dots\ in}\\
-  Analogous to  {\tt rewrite {\term}} but rewriting is done in the
-  hypothesis named {\ident}.
+  Analogous to {\tt rewrite {\term}} but rewriting is done following
+  {\clause} (similarly to \ref{Conversion-tactic}). For instance:
+  \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1;
+    rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do
+  \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <>
+    H}.
 
 \item {\tt rewrite -> {\term} in {\ident}}
   \tacindex{rewrite -> \dots\ in}\\
@@ -1656,12 +1679,12 @@ goal stating ``$eq$ {\term} {\term}$_1$''.
 Lemmas are added to the database using the command 
 \comindex{Declare Left Step}
 \begin{quote}
-{\tt Declare Left Step {\qualid}.}
+{\tt Declare Left Step {\term}.}
 \end{quote}
-where {\qualid} is the name of the lemma.
 
 The tactic is especially useful for parametric setoids which are not
-accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}).
+accepted as regular setoids for {\tt rewrite} and {\tt
+  setoid\_replace} (see chapter \ref{setoid_replace}).
 
 \tacindex{stepr}
 \comindex{Declare Right Step}
@@ -1677,7 +1700,7 @@ Lemmas are expected to be of the form
 $z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
 and are registered using the command
 \begin{quote}
-{\tt Declare Right Step {\qualid}.}
+{\tt Declare Right Step {\term}.}
 \end{quote}
 \end{Variants}
 
@@ -2746,7 +2769,7 @@ of the reengineering of the code, this tactic has also been completely revised
 to get a very compact and readable version.} carries out rewritings according
 the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
 
- Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
+Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
 it fails. Once all the rules have been processed, if the main subgoal has
 progressed (e.g., if it is distinct from the initial main goal) then the rules
 of this base are processed again. If the main subgoal has not progressed then
@@ -2762,12 +2785,11 @@ command.
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
-%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\
-%{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\
-%These are deprecated syntactic variants for
-%{\tt autorewrite with \ident$_1$ \dots \ident$_n$}
-%and
-%{\tt autorewrite  with \ident$_1$ \dots \ident$_n$ using \tac}.
+
+\item \texttt{autorewrite with {\ident} in {\qualid}}
+
+  Performs all the rewritings in hypothesis {\qualid}.
+
 \end{Variant}
 
 \subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident