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 /plugins/setoid_ring | |
| 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 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index f6f751268..4822a0c99 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -604,7 +604,8 @@ Section MakeRingPol. (morph_opp CRmorph) : Esimpl. - Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl. + (* Quicker than autorewrite with Esimpl :-) *) + Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl. Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c]. Proof. |