diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/EnvRing.v | 3 |
1 files changed, 2 insertions, 1 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. |