diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 14 |
2 files changed, 10 insertions, 8 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6a794e9eb..342b20cb5 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} diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 2e515a9a6..a4e5d4cb8 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -323,19 +323,21 @@ GEXTEND Gram [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; rewriter : - [ [ c = constr_with_bindings -> (Precisely 1, c) - | "!"; c = constr_with_bindings -> (RepeatPlus,c) - | "?"; c = constr_with_bindings -> (RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) - | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c) + [ [ (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally produce a pattern_ident *) - | c = pattern_ident -> + c = pattern_ident -> let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in (RepeatStar, c) | n = natural; c = pattern_ident -> let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in (UpTo n, c) + | "!"; c = constr_with_bindings -> (RepeatPlus,c) + | "?"; c = constr_with_bindings -> (RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) + | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c) + | n = natural; c = constr_with_bindings -> (Precisely n,c) + | c = constr_with_bindings -> (Precisely 1, c) ] ] ; oriented_rewriter : |