revision de la semantique de rewrite ... in <clause>. details dans la doc

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

1 files changed, 20 insertions, 10 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b491cc3d4..315286571 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1584,20 +1584,30 @@ This happens if \term$_1$ does not occur in the goal.
 \item {\tt rewrite {\term} in \textit{clause}}
   \tacindex{rewrite \dots\ in}\\
   Analogous to {\tt rewrite {\term}} but rewriting is done following
-  \textit{clause} (similarly to \ref{Conversion-tactics}). 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}}
+  \textit{clause} (similarly to \ref{Conversion-tactics}). For
+  instance:
+  \begin{itemize}
+  \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
+    \texttt{H1} instead of the current goal.
+  \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
+      rewrite H in H2}. In particular a failure will happen if any of
+    these three simplier tactics fails. 
+  \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
+      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+    as soon as at least one of these simplier tactics succeeds.
+  \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} 
+    and \texttt{rewrite H in * |-} that succeeds if at
+    least one of these two tactics succeeds. 
+  \end{itemize}
+
+\item {\tt rewrite -> {\term} in \textit{clause}}
   \tacindex{rewrite -> \dots\ in}\\
-  Behaves as {\tt rewrite {\term} in {\ident}}.
+  Behaves as {\tt rewrite {\term} in \textit{clause}}.
  
-\item {\tt rewrite <- {\term} in {\ident}}\\
+\item {\tt rewrite <- {\term} in \textit{clause}}\\
   \tacindex{rewrite <- \dots\ in}
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
-  rewrite in the hypothesis named {\ident}.
+  rewrite in \textit{clause} as explained above.
 \end{Variants}