diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-06 15:16:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-06 15:16:31 +0000 |
| commit | 21ef8f6d6679c0f6865313eb5c0dec166a5fdb61 (patch) | |
| tree | ae9f9958fc4be9ab4ad58df6c86a5d8ba85aa05b /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 14 |
1 files changed, 8 insertions, 6 deletions
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 : |