aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:27:54 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:27:54 +0100
commited05111e048e864c63c2e21b8ebac675a80dc464 (patch)
tree47e7bb219ba43e901b2bfc3791e80f161246dd54 /doc
parent5003953d45ea0e780cd50bb9d6521799adf18079 (diff)
parent711b9d8cdf6e25690d247d9e8c49f005527e64e2 (diff)
Merge PR #915: Fix rewrite in * side conditions
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-tac.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9635b3ab1..6dca314b4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal.
rewrite H in H2 at - 2}. In particular a failure will happen if any of
these three simpler tactics fails.
\item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
- H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+ H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen
as soon as at least one of these simpler tactics succeeds.
\item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
and \texttt{rewrite H in * |-} that succeeds if at