1 files changed, 27 insertions, 17 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a58125dc09..6a794e9eb3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1756,7 +1756,7 @@ 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$)}\texttt{eq}\term$_1$ \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.
@@ -1781,9 +1781,11 @@ This happens if \term$_1$ does not occur in the goal.
 
 \begin{Variants}
 \item {\tt rewrite -> {\term}}\tacindex{rewrite ->}\\
+  {\tt rewrite +{\term}}\tacindex{rewrite +}\\
   Is equivalent to {\tt rewrite \term}
 
 \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
+  {\tt rewrite -{\term}}\tacindex{rewrite -}\\
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
 \item {\tt rewrite {\term} in \textit{clause}}
@@ -1804,24 +1806,32 @@ This happens if \term$_1$ does not occur in the goal.
     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 \textit{clause}}.
- 
-\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 \textit{clause} as explained above.
+  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  inserted before the term to rewrite.
 
 \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. 
+  Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
+  up to {\tt rewrite $\term_n$}, each one working on the first subgoal
+  generated by the previous one.
+  Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
+  inserted before each term to rewrite. One unique \textit{clause}
+  can be added at the end after the keyword {\tt in}, it will 
+  then affect all rewrite operations.
+
+\item In all forms of {\tt rewrite} described above, a term to rewrite
+  can be immediately prefixed by one of the following modifiers:
+  \begin{itemize}
+  \item {\tt ?} : the tactic {\tt rewrite ?$\term$} performs the
+    rewrite of $\term$  as many times as possible (perhaps zero time).
+    This form never fails. 
+  \item {\tt $n$?} : works similarly, except that it will do at most 
+   $n$ rewrites. 
+  \item {\tt !} : works as {\tt ?}, except that at least one rewrite 
+    should succeed, otherwise the tactic fails. 
+  \item {\tt $n$!} : precisely $n$ rewrites of $\term$ will be done, 
+    leading to failure if these $n$ rewrites are not possible. 
+  \end{itemize}
+
 
 \end{Variants}