Ajout stepl et stepr

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

1 files changed, 38 insertions, 0 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 1673ceb88..5c78dcdec 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1506,6 +1506,44 @@ When several hypotheses have the form {\tt \ident=t} or {\tt
     for which an equality exists.
 \end{Variants}
 
+\subsection{{\tt stepl {\term}}}
+\tacindex{stepl}
+
+This tactic is for chaining rewriting steps. It assumes a goal of the
+form ``$R$ {\term}$_1$ {\term}$_2$'' where $R$ is a binary relation
+and relies on a database of lemmas of the form {\tt forall} $x$ $y$
+$z$, $R$ $x$ $y$ {\tt ->} $eq$ $x$ $z$ {\tt ->} $R$ $z$ $y$ where $eq$
+is typically a setoid equality. The application of {\tt stepl {\term}}
+then replaces the goal by ``$R$ {\term} {\term}$_2$'' and adds a new
+goal stating ``$eq$ {\term} {\term}$_1$''.
+
+Lemmas are added to the database using the command 
+\comindex{Declare Left Step}
+\begin{quote}
+{\tt Declare Left Step {\qualid}.}
+\end{quote}
+where {\qualid} is the name of the lemma.
+
+The tactic is especially useful for parametric setoids which are not
+accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}).
+
+\tacindex{stepr}
+\comindex{Declare Right Step}
+\begin{Variants}
+\item{\tt stepl {\term} by {\tac}}\\
+This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
+
+\item{\tt stepr {\term}}\\
+     {\tt stepr {\term} by {\tac}}\\
+This behaves as {\tt stepl} but on the right-hand-side of the binary relation.
+Lemmas are expected to be of the form
+``{\tt forall} $x$ $y$
+$z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
+and are registered using the command
+\begin{quote}
+{\tt Declare Right Step {\qualid}.}
+\end{quote}
+\end{Variants}
 
 \section{Equality and inductive sets}