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/fingroup/fingroup.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'mathcomp/fingroup') 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]. -- cgit v1.2.3