diff options
| author | Anton Trunov | 2018-11-16 10:55:30 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-12-04 14:25:53 +0100 |
| commit | 79aa2b1ab5b233f103cd3e402094cd93d9028866 (patch) | |
| tree | 4d3afa56b14db2de71dbd52c959e71c9766e66fb /ChangeLog | |
| parent | e99b8b9695cdb53492e63077cb0dd551c4a06dc3 (diff) | |
Remove `_ : Type` from packed classes
This increases performance 10% - 15% for Coq v8.6.1 - v8.9.dev.
Tested on a Debain-based 16-core build server and
a Macbook Pro laptop with 2,3 GHz Intel Core i5.
| | Compilation time, old | Compilation | Speedup |
| | (mathcomp commit 967088a6f87) | time, new | |
| Coq 8.6.1 | 10min 33s | 9min 10s | 15% |
| Coq 8.7.2 | 10min 12s | 8min 50s | 15% |
| Coq 8.8.2 | 9min 39s | 8min 32s | 13% |
| Coq 8.9.dev(05d827c800544) | 9min 12s | 8min 16s | 11% |
| | | | |
It seems Coq at some point fixed the problem `_ : Type` was
supposed to solve.
Diffstat (limited to 'ChangeLog')
0 files changed, 0 insertions, 0 deletions