From 711b9d8cdf6e25690d247d9e8c49f005527e64e2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 21 Jul 2017 13:43:31 +0200 Subject: Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". Noticed by Sigurd Schneider. --- doc/refman/RefMan-tac.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 66a5f107a..bf30a3051 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 -- cgit v1.2.3