diff options
| author | Cyril Cohen | 2018-12-10 18:31:46 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-10 18:31:46 +0100 |
| commit | 67ccc34eb6f05383e0e7bd90c7df9e4fb51f2a87 (patch) | |
| tree | a54cd823592f397d744fb7c17449c1d6a333ab74 /mathcomp/fingroup | |
| parent | e99b8b9695cdb53492e63077cb0dd551c4a06dc3 (diff) | |
| parent | 7ae08ee81c6859fb7ee4043207d87572a4bc3bc3 (diff) | |
Merge pull request #248 from anton-trunov/remove-Type-from-packed-classes
Remove `_ : Type` from packed classes
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]. |