diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-23 08:20:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-23 08:20:32 +0000 |
| commit | 911b8eb0ca662ff84350fab907c797016ef795d5 (patch) | |
| tree | 9be13ceb4b0b5719731dfdf539c4ec4c4b22db70 | |
| parent | 2a759658f8c31218da576502d4bd06dcc69026a0 (diff) | |
Typos et passage v7->v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8482 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/Setoid.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/Setoid.tex b/doc/Setoid.tex index de39331e4..867d60366 100644 --- a/doc/Setoid.tex +++ b/doc/Setoid.tex @@ -12,7 +12,7 @@ Leibniz equality does not denote the intended equality. For example using lists to denote finite sets drive to difficulties since two non convertible terms can denote the same set. -We present here a \Coq\ module, {\tt setoid\_replace}, which allow to +We present here a \Coq\ module, {\tt setoid\_replace}, which allows to structure and automate some parts of the work. In particular, if everything has been registered a simple tactic can do replacement just as if the two terms were equal. @@ -119,7 +119,7 @@ compatibility lemma. \item \errindex{The term \term \ should not be a dependent product} \end{ErrMsgs} -The compatibility lemma genereted depends on the setoids already +The compatibility lemma generated depends on the setoids already declared. \asection{The tactic itself} @@ -133,10 +133,10 @@ use the tactic called \texttt{setoid\_replace}. The syntax is \texttt{setoid\_replace} $ term_1$ with $term_2$ \end{quotation} -The effect is similar to the one of \texttt{Replace}. +The effect is similar to the one of \texttt{replace}. You also have a tactic called \texttt{setoid\_rewrite} which is the -equivalent of \texttt{Rewrite} for setoids. The syntax is +equivalent of \texttt{rewrite} for setoids. The syntax is \begin{quotation} \texttt{setoid\_rewrite} \term @@ -147,8 +147,8 @@ equivalent of \texttt{Rewrite} for setoids. The syntax is \item \texttt{setoid\_rewrite <-} \term \end{Variants} -The arrow tells the systems in which direction the rewriting has to be -done. Moreover, you can use \texttt{Rewrite} for setoid +The arrow tells the system in which direction the rewriting has to be +done. Moreover, you can use \texttt{rewrite} for setoid rewriting. In that case the system will check if the term you give is an equality or a setoid equivalence and do the appropriate work. |