diff options
Diffstat (limited to 'doc/refman')
| -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 6a794e9eb3..342b20cb57 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1828,8 +1828,8 @@ This happens if \term$_1$ does not occur in the goal. $n$ rewrites. \item {\tt !} : works as {\tt ?}, except that at least one rewrite should succeed, otherwise the tactic fails. - \item {\tt $n$!} : precisely $n$ rewrites of $\term$ will be done, - leading to failure if these $n$ rewrites are not possible. + \item {\tt $n$!} (or simply {\tt $n$}) : precisely $n$ rewrites + of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. \end{itemize} |