From ae42e00f886f7c2ef743e2fdd58c55b5c3acdd87 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 11 Sep 2014 20:53:13 +0200 Subject: Use an AST for strategy names. --- tactics/rewrite.mli | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'tactics/rewrite.mli') 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 -- cgit v1.2.3