MAJ Simpl et Change

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

1 files changed, 21 insertions, 1 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index fb2240123d..9c553473cb 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -541,9 +541,18 @@ convertible.
 \item \errindex{Not convertible}
 \end{ErrMsgs}
 
+\tacindex{Change \dots\ in}
 \begin{Variants}
+\item {\tt Change \term$_1$ with \term$_2$} \\
+This replaces the occurrences of \term$_1$ by \term$_2$ in the current goal.
+The terms \term$_1$ and \term$_2$ must be convertible.
+\item {\tt Change \num$_1$ \dots\ \num$_i$ \term$_1$ with \term$_2$} \\
+This replaces the occurrences numbered \num$_1$ \dots\ \num$_i$ of \term$_1$ by \term$_2$ in the current goal.
+The terms \term$_1$ and \term$_2$ must be convertible.\\
+\ErrMsg {\tt Too few occurrences}
 \item {\tt Change {\term} in {\ident}}\\ 
-  \tacindex{Change \dots\ in}
+\item {\tt Change \term$_1$ with \term$_2$ in {\ident}}\\ 
+\item {\tt Change \num$_1$ \dots\ \num$_i$ \term$_1$ with \term$_2$ in {\ident}}\\ 
   This applies the {\tt Change} tactic not to the goal but to the
   hypothesis {\ident}.
 \end{Variants}
@@ -702,6 +711,17 @@ $\beta\iota$ rules. But when the $\iota$ rule is not applicable then
 possible $\delta$-reductions are not applied.  For instance trying to
 use {\tt Simpl} on {\tt (plus n O)=n} will change nothing.
 
+\tacindex{Simpl \dots\ in}
+\begin{Variants}
+\item {\tt Simpl {\term}}\\ 
+This applies {\tt Simpl} only to the occurrences of {\term} in the
+current goal.
+\item {\tt Simpl \num$_1$ \dots\ \num$_i$ {\term}}\\ 
+This applies {\tt Simpl} only to the \num$_1$, \dots, \num$_i$ 
+occurrences of {\term} in the current goal.\\
+\ErrMsg {\tt Too few occurrences}
+\end{Variants}
+
 \subsection{\tt Unfold \qualid}
 \tacindex{Unfold}\label{Unfold}
 This tactic applies to any goal. The argument {\qualid} must denote