diff options
| -rw-r--r-- | tactics/g_rewrite.ml4 | 4 | ||||
| -rw-r--r-- | tactics/rewrite.mli | 27 |
2 files changed, 4 insertions, 27 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index e52a79b55..f4c5aeda8 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -108,8 +108,8 @@ END (* By default the strategy for "rewrite_db" is top-down *) -let db_strat db = Strategies.td (Strategies.hints db) -let cl_rewrite_clause_db db cl = cl_rewrite_clause_strat (db_strat db) cl +let db_strat db = StratUnary ("topdown", StratHints (false, db)) +let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) TACTIC EXTEND rewrite_strat | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index e18a2b271..4d1e285f9 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -28,32 +28,9 @@ type ('constr,'redexpr) strategy_ast = | StratEval of 'redexpr | StratFold of 'constr -type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) +type strategy -type rewrite_proof = - | RewPrf of constr * constr - | RewCast of cast_kind - -type rewrite_result_info = { - rew_car : constr; - rew_from : constr; - rew_to : constr; - rew_prf : rewrite_proof; - rew_evars : evars; -} - -type rewrite_result = rewrite_result_info option - -type strategy = env -> Id.t list -> constr -> types -> - constr option -> evars -> rewrite_result option - -module Strategies : -sig - val td : strategy -> strategy - val hints : string -> strategy -end - -val strategy_of_ast : (Glob_term.glob_constr * 'a, raw_red_expr) strategy_ast -> strategy +val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast |