Rework on rich forms of rewrite

 1) changed the semantics of rewrite H,H' : the earlier semantics 
    (rewrite H,H' == rewrite H; rewrite H') was poorly suited for 
    situations where first rewrite H generates side-conditions. 
    New semantics is tclTHENFIRST instead of tclTHEN, that is
    side-conditions are left untouched. 

    Note to myself: check if side-effect-come-first bug of 
    setoid rewrite is still alive, and do something if yes

 2) new syntax for rewriting something many times. This syntax is 
    shamelessly taken from ssreflect: 

    rewrite ?H  means "H as many times as possible" 
      (i.e. almost repeat rewrite H, except that 
       possible side-conditions are left apart as in 1)
    rewrite !H  means "at least once" (i.e. rewrite H; repeat rewrite H)
    rewrite 3?H means "up to 3 times", maybe less 
      (i.e. something like: do 3 (try rewrite H)).
    rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H).

    For instance:  rewrite 3?foo, <-2!bar in H1,H2|-*

 3) By the way, for a try, I've enabled the syntax +/- as synonyms for 
    ->/<- in the orientation of rewrite. 
   
   Comments welcome ...




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

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}