diff options
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 01eea88..70553a0 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -232,7 +232,7 @@ Structure base_type : Type := PackBase { (* coercion of A * B to pred_sort in x \in A * B, or rho * tau to *) (* ffun and Funclass in (rho * tau) x, when rho tau : perm T. *) (* Therefore we define an alias of sort for argument types, and *) -(* make it the default coercion FinGroup.base_class >-> Sortclass *) +(* make it the default coercion FinGroup.base_type >-> Sortclass *) (* so that arguments of a functions whose parameters are of type, *) (* say, gT : finGroupType, can be coerced to the coercion class *) (* of arg_sort. Care should be taken, however, to declare the *) |