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/ssreflect/eqtype.v | |
| 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/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 7473ed7..a5e8784 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -126,13 +126,13 @@ Notation class_of := mixin_of (only parsing). Section ClassDef. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ := cT return class_of cT in c. +Definition class := let: Pack _ c := cT return class_of cT in c. -Definition pack c := @Pack T c T. +Definition pack c := @Pack T c. Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c. End ClassDef. |