diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-26 20:15:20 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-26 20:15:20 +0000 |
commit | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (patch) | |
tree | 490a24b0a73e9281de4c26457d17851e0db7c6c3 | |
parent | 5ebb6f58d2906e53b0de5c7f687dd6e338aa62a2 (diff) |
Opacifying the type of strategies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16805 85f007b7-540e-0410-9357-904b9bb8a0f7
-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 |