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 /mathcomp/fingroup | |
| 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 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index a68bc9f..19cefcd 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -302,10 +302,10 @@ Local Notation T := (arg_sort bT). Local Notation rT := (sort bT). Local Notation class := (finClass bT). -Canonical eqType := Equality.Pack class rT. -Canonical choiceType := Choice.Pack class rT. -Canonical countType := Countable.Pack class rT. -Canonical finType := Finite.Pack class rT. +Canonical eqType := Equality.Pack class. +Canonical choiceType := Choice.Pack class. +Canonical countType := Countable.Pack class. +Canonical finType := Finite.Pack class. Definition arg_eqType := Eval hnf in [eqType of T]. Definition arg_choiceType := Eval hnf in [choiceType of T]. Definition arg_countType := Eval hnf in [countType of T]. |