From 79aa2b1ab5b233f103cd3e402094cd93d9028866 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Fri, 16 Nov 2018 10:55:30 +0100
Subject: 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.
---
 mathcomp/ssreflect/eqtype.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/eqtype.v')

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.
-- 
cgit v1.2.3


From efbcb84f3ddfea53b7b914284d8fa80fdb7a56fd Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Fri, 23 Nov 2018 10:16:12 +0100
Subject: Remove pack constructors

---
 mathcomp/ssreflect/eqtype.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/eqtype.v')

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index a5e8784..6ed4b97 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -132,8 +132,7 @@ Variables (T : Type) (cT : type).
 
 Definition class := let: Pack _ c := cT return class_of cT in c.
 
-Definition pack c := @Pack T c.
-Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.
+Definition clone := fun c & cT -> T & phant_id (@Pack T c) cT => Pack c.
 
 End ClassDef.
 
@@ -141,7 +140,7 @@ Module Exports.
 Coercion sort : type >-> Sortclass.
 Notation eqType := type.
 Notation EqMixin := Mixin.
-Notation EqType T m := (@pack T m).
+Notation EqType T m := (@Pack T m).
 Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T)
   (at level 0, format "[ 'eqMixin'  'of'  T ]") : form_scope.
 Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id)
-- 
cgit v1.2.3