diff options
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 f6f7512683..4822a0c993 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. |