diff options
| author | letouzey | 2012-07-05 16:56:46 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-05 16:56:46 +0000 |
| commit | 819029226c334030a540ed7570bc423c4463c6b4 (patch) | |
| tree | 5196fc485aee98f03c4d78aece6e4ff1a9511ee5 /tactics | |
| parent | 6a3ad48eee6ef6d067708f4484fa29efb0476da7 (diff) | |
rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite
rewrite_db fails if nothing has been rewritten, and it only performs
*one* top-down pass. For the moment, use (repeat rewrite_db) for
emulating more closely autorewrite.
Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend
with fun(ny) parts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 2e7aed2b32..532f36c15e 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1528,9 +1528,16 @@ ARGUMENT EXTEND rewstrategy | [ "fold" constr(c) ] -> [ StratFold c ] 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 + TACTIC EXTEND rewrite_strat | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] | [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] +| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] END let clsubstitute o c = |