diff options
Diffstat (limited to 'plugins/ltac/g_tactic.ml4')
| -rw-r--r-- | plugins/ltac/g_tactic.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index dc9f607cf..15db4ca6a 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -494,12 +494,12 @@ GEXTEND Gram | -> None ] ] ; rewriter : - [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c) - | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,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_arg -> (Precisely 1, c) + [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c) + | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c) + | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c) + | c = constr_with_bindings_arg -> (Equality.Precisely 1, c) ] ] ; oriented_rewriter : |