diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 14:30:25 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 14:30:25 +0000 |
| commit | e0f1235531b94301459e3b8eb2746e66258c832c (patch) | |
| tree | 3b95cb0305074d07d2d04212ef4d923a78f42d47 /doc | |
| parent | 2bbec9bbe0aeb472e2596cebc7f76c724a8c807a (diff) | |
Typo dans le manuel de référence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 93a7406eb..aaa2ee51f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1555,10 +1555,10 @@ This happens if \term$_1$ does not occur in the goal. \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\ Uses the equality \term$_1${\tt=}\term$_2$ from right to left -\item {\tt rewrite {\term} in {\clause}} +\item {\tt rewrite {\term} in \textit{clause}} \tacindex{rewrite \dots\ in}\\ Analogous to {\tt rewrite {\term}} but rewriting is done following - {\clause} (similarly to \ref{Conversion-tactic}). For instance: + \textit{clause} (similarly to \ref{Conversion-tactic}). For instance: \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1; rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <> |