diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/EnvRing.v | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index c172157f1..e1424bb10 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -617,7 +617,8 @@ Qed. (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. 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. |