diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 20:53:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-11 20:53:13 +0200 |
| commit | ae42e00f886f7c2ef743e2fdd58c55b5c3acdd87 (patch) | |
| tree | 841be5cc3ceb8d065408bb5ed2355f9fa4d73e63 /tactics/g_rewrite.ml4 | |
| parent | 580b25e05c7cc9e7a31430b3d9edb14ae12b7598 (diff) | |
Use an AST for strategy names.
Diffstat (limited to 'tactics/g_rewrite.ml4')
| -rw-r--r-- | tactics/g_rewrite.ml4 | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index b715be9e6..5c46fdf2a 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -79,22 +79,22 @@ ARGUMENT EXTEND rewstrategy [ glob(c) ] -> [ StratConstr (c, true) ] | [ "<-" constr(c) ] -> [ StratConstr (c, false) ] - | [ "subterms" rewstrategy(h) ] -> [ StratUnary ("all_subterms", h) ] - | [ "subterm" rewstrategy(h) ] -> [ StratUnary ("one_subterm", h) ] - | [ "innermost" rewstrategy(h) ] -> [ StratUnary("innermost", h) ] - | [ "outermost" rewstrategy(h) ] -> [ StratUnary("outermost", h) ] - | [ "bottomup" rewstrategy(h) ] -> [ StratUnary("bottomup", h) ] - | [ "topdown" rewstrategy(h) ] -> [ StratUnary("topdown", h) ] + | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ] + | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ] + | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ] + | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ] + | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ] + | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ] | [ "id" ] -> [ StratId ] | [ "fail" ] -> [ StratFail ] | [ "refl" ] -> [ StratRefl ] - | [ "progress" rewstrategy(h) ] -> [ StratUnary ("progress", h) ] - | [ "try" rewstrategy(h) ] -> [ StratUnary ("try", h) ] - | [ "any" rewstrategy(h) ] -> [ StratUnary ("any", h) ] - | [ "repeat" rewstrategy(h) ] -> [ StratUnary ("repeat", h) ] - | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary ("compose", h, h') ] + | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ] + | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ] + | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ] + | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ] + | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ] | [ "(" rewstrategy(h) ")" ] -> [ h ] - | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary ("choice", h, h') ] + | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ] | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ] | [ "hints" preident(h) ] -> [ StratHints (false, h) ] | [ "terms" constr_list(h) ] -> [ StratTerms h ] |