Use [rewrite] rather than [change] to speed up Qed

[Opaque] tells kernel unification to defer unfolding a constant as long as
possible.  This is not a problem for [change], when the functions are small and
directly convertible.  It's disastrous for [Qed]/[Defined], which (if I
understand correctly) try to unify [Opaquemul x' y'] with [mul x y] by fully
unfolding [mul] and [x] and [y] before trying to unfold [Opaquemul]; when [x]
and [y] are large, this takes a very long time.

Rewrite avoids this by telling Coq *how* to unify [Opaquemul x' y'] with [mul x
y] (namely, by unifying [Opaquemul] with [mul], and then [x] with [x'] and [y]
with [y']).

0 files changed, 0 insertions, 0 deletions