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/algebra/vector.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'mathcomp/algebra/vector.v') diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 542f8ad..75b2073 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -117,27 +117,27 @@ Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V). Structure class_of V := Class { base : GRing.Lmodule.class_of R V; - mixin : mixin_of (GRing.Lmodule.Pack _ base V) + mixin : mixin_of (GRing.Lmodule.Pack _ base) }. Local Coercion base : class_of >-> GRing.Lmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ := cT return class_of cT in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c := cT return class_of cT in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition dim := let: Mixin n _ := mixin class in n. -Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0 T)) := +Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) := fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b => - fun m & phant_id m0 m => Pack phR (@Class T b m) T. + fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. End ClassDef. Notation axiom n V := (axiom_def n (Phant V)). -- cgit v1.2.3