Module Ltac_plugin.RewriteStratAst

type unary_strategy =
| Subterms
| Subterm
| Innermost
| Outermost
| Bottomup
| Topdown
| Progress
| Try
| Any
| Repeat
type binary_strategy =
| Compose
type nary_strategy =
| Choice
type ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast =
| StratId
| StratFail
| StratRefl
| StratUnary of unary_strategy * ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast
| StratBinary of binary_strategy * ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast * ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast
| StratNAry of nary_strategy * ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast list
| StratConstr of 'constr * bool
| StratTerms of 'constr list
| StratHints of bool * string
| StratEval of 'redexpr
| StratFold of 'constr
| StratVar of 'id
| StratFix of 'id * ('constr, 'constr_pattern, 'redexpr, 'id, 'tactic) strategy_ast
| StratMatches of 'constr_pattern
| StratTactic of 'tactic
val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('e -> 'f) -> ('g -> 'h) -> ('i -> 'j) -> ('a, 'c, 'e, 'g, 'i) strategy_ast -> ('b, 'd, 'f, 'h, 'j) strategy_ast
val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('d -> Pp.t) -> ('e -> Pp.t) -> ('a, 'b, 'c, 'd, 'e) strategy_ast -> Pp.t