diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:46 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:46 +0000 |
| commit | 819029226c334030a540ed7570bc423c4463c6b4 (patch) | |
| tree | 5196fc485aee98f03c4d78aece6e4ff1a9511ee5 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions