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/rewrite.mli | |
| parent | 580b25e05c7cc9e7a31430b3d9edb14ae12b7598 (diff) | |
Use an AST for strategy names.
Diffstat (limited to 'tactics/rewrite.mli')
| -rw-r--r-- | tactics/rewrite.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 926081bbb..05eff00bb 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -18,10 +18,18 @@ open Tacinterp (** TODO: document and clean me! *) +type unary_strategy = + Subterms | Subterm | Innermost | Outermost + | Bottomup | Topdown | Progress | Try | Any | Repeat + +type binary_strategy = + | Compose | Choice + type ('constr,'redexpr) strategy_ast = | StratId | StratFail | StratRefl - | StratUnary of string * ('constr,'redexpr) strategy_ast - | StratBinary of string * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast + | StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast + | StratBinary of binary_strategy + * ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast | StratConstr of 'constr * bool | StratTerms of 'constr list | StratHints of bool * string |