diff options
| author | letouzey | 2008-03-06 15:16:31 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-06 15:16:31 +0000 |
| commit | 21ef8f6d6679c0f6865313eb5c0dec166a5fdb61 (patch) | |
| tree | ae9f9958fc4be9ab4ad58df6c86a5d8ba85aa05b /doc | |
| parent | 07ffd30a82ebfe35811ca43d71aeacdb86f4cc87 (diff) | |
repair for commit 10612 (due to grammar order, some syntaxes weren't working)
and add a simpler synonym for "exactly N times" :
rewrite 3 H (or rewrite 3H) means rewrite 3!H
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10629 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 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} |