3 files changed, 27 insertions, 10 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index fc5f4e4cb6..7ef9078db4 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -832,7 +832,7 @@ possible with the syntax:
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
 \end{quote}
-
+\medskip
 It is also possible to \emph{redefine} an existing user-defined tactic
 using the syntax:
 \begin{quote}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5ccbaf1302..44c519e997 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2008,16 +2008,18 @@ must have the form
 \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
+\noindent Then {\tt rewrite \term} finds the first subterm matching
+\term$_1$ in the goal, resulting in instances \term$_1'$ and \term$_2'$
+and then replaces every occurrence of \term$_1'$ by \term$_2'$.
+Hence, some of the variables x$_i$ are
 solved by unification, and some of the types \texttt{A}$_1$, \dots,
 \texttt{A}$_n$ become new subgoals.
 
-\Rem In case the type of  
-\term$_1$ contains occurrences of variables bound in the
-type of \term, the tactic tries first to find a subterm of the goal
-which matches this term in order to find a closed instance \term$'_1$
-of \term$_1$, and then all instances of \term$'_1$ will be replaced.
+% \Rem In case the type of  
+% \term$_1$ contains occurrences of variables bound in the
+% type of \term, the tactic tries first to find a subterm of the goal
+% which matches this term in order to find a closed instance \term$'_1$
+% of \term$_1$, and then all instances of \term$'_1$ will be replaced.
 
 \begin{ErrMsgs}
 \item \errindex{The term provided does not end with an equation}
@@ -2056,6 +2058,21 @@ This happens if \term$_1$ does not occur in the goal.
   Orientation {\tt ->} or {\tt <-} (or {\tt +} or {\tt -}) can be
   inserted before the term to rewrite.
 
+\item {\tt rewrite {\term} at \textit{occurrences}}
+  \tacindex{rewrite \dots\ at}
+
+  Rewrite only the given occurrences of \term$_1'$. Occurrences are
+  specified from left to right as for \texttt{pattern} (\S
+  \ref{pattern}). The rewrite is always performed using setoid
+  rewriting, even for leibniz equality, so one has to 
+  \texttt{Import Setoid} to use this variant.
+
+\item {\tt rewrite {\term} by {\tac}}
+  \tacindex{rewrite \dots\ by}
+
+  Use {\tac} to completely solve the side-conditions arising from the
+  rewrite.
+
 \item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
   Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
   up to {\tt rewrite $\term_n$}, each one working on the first subgoal
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 8bdf6ab0a2..d2b6d11516 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -540,7 +540,7 @@ the prefixed tactics it is possible to pass additional arguments such as
 
 The \texttt{using relation}
 arguments cannot be passed to the unprefixed form. The latter argument
-tells the  tactic what parametric  relation should be used  to replace
+tells the tactic what parametric relation should be used to replace
 the first tactic argument with the second one. If omitted, it defaults
 to the \texttt{DefaultRelation} instance on the type of the objects.
 By default, it means the most recent \texttt{Equivalence} instance in
@@ -679,7 +679,7 @@ If a signature mentions a relation $R$ on the left of an arrow
 is smaller than $R$, and the inverse applies on the right of an arrow. 
 One can then declare only a few morphisms instances that generate the complete set
 of signatures for a particular constant. By default, the only declared
-subrelations is \texttt{iff}, which is a subrelation of \texttt{impl}
+subrelation is \texttt{iff}, which is a subrelation of \texttt{impl}
 and \texttt{inverse impl} (the dual of implication). That's why we can
 declare only two morphisms for conjunction:
 \verb|Morphism (impl ==> impl ==> impl) and| and