diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 11:47:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 11:58:21 +0100 |
| commit | 1aecaf88e5491d29b200515fc64ce3d479318758 (patch) | |
| tree | 8c6824c514b30badfb25e22a2ebe42104c22cf9b /parsing | |
| parent | 3c2dc887a8b4cae06a55f3b3ae2b6186a6056f1a (diff) | |
Tactics: Generalizing the use of the experimental clearing modifier to
all cases of rewrite.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 3d59b9b8d..3e4a6c6a1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -240,7 +240,7 @@ GEXTEND Gram [ [ n = natural -> (None,ElimOnAnonHyp n) | test_lpar_id_rpar; c = constr_with_bindings -> (Some false,induction_arg_of_constr c) - | c = constr_with_bindings -> (None,induction_arg_of_constr c) + | c = constr_with_bindings_arg -> on_snd induction_arg_of_constr c ] ] ; constr_with_bindings_arg: @@ -499,12 +499,12 @@ GEXTEND Gram [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; rewriter : - [ [ "!"; c = constr_with_bindings -> (RepeatPlus,(None,c)) + [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings -> (Precisely n,(None,c)) + | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c) | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c) | n = natural; c = constr_with_bindings_arg -> (Precisely n,c) - | c = constr_with_bindings -> (Precisely 1, (None,c)) + | c = constr_with_bindings_arg -> (Precisely 1, c) ] ] ; oriented_rewriter : |