Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Improve performance of Strings/Byte.v
from
Byte.vo (real: 3.78, user: 3.74, sys: 0.04, mem: 470260 ko)
to
Byte.vo (real: 1.96, user: 1.91, sys: 0.04, mem: 467360 ko)
by using do ... refine with an appropriate lemma instead of an ad-hoc repeat match goal with.
Since only some proofs are touched, no changelog needed.
Improve performance of
Strings/Byte.vfromByte.vo (real: 3.78, user: 3.74, sys: 0.04, mem: 470260 ko)toByte.vo (real: 1.96, user: 1.91, sys: 0.04, mem: 467360 ko)by usingdo ... refinewith an appropriate lemma instead of an ad-hocrepeat match goal with.Since only some proofs are touched, no changelog needed.