Adding a syntax for "n-ary" rewrite:

 
 rewrite H, H'

means: rewrite H; rewrite H'. 

This should still be compatible with other "features" of rewrite: like
orientation, implicit arguments (t:=...), and "in" clause.  Concerning
the "in" clause, for the moment only one is allowed at the very end of
the tactic, and it applies to all the different rewrites that are
done. For instance, if someone _really_ wants to use all features at
the same time:

 rewrite H1 with (t:=u), <-H2, H3  in *

means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in *




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

1 files changed, 10 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0ba9553ce..8dd168aad 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1728,6 +1728,16 @@ This happens if \term$_1$ does not occur in the goal.
   \tacindex{rewrite <- \dots\ in}
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
   rewrite in \textit{clause} as explained above.
+
+\item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
+  Is equivalent to {\tt rewrite $\term_1$; \ldots; rewrite $\term_n$}.
+  Orientation {\tt ->} or {\tt <-} can be inserted before each term. 
+  
+\item {\tt rewrite $\term_1$, \ldots, $term_n$ in \textit{clause}}\\
+  Is equivalent to {\tt rewrite $\term_1$ in \textit{clause}; \ldots; 
+  rewrite $\term_n$ in \textit{clause}}.
+  Orientation {\tt ->} or {\tt <-} can be inserted before each term. 
+
 \end{Variants}