aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/character/mxrepresentation.v
diff options
context:
space:
mode:
authorGeorges Gonthier2018-11-26 19:51:27 +0100
committerGeorges Gonthier2018-11-26 19:51:27 +0100
commit03ad994dfee48e1a7b2b7091c45dfdcf4402f826 (patch)
treed891c2b8507452f2aaac1cbfe7dfbb709e751629 /mathcomp/character/mxrepresentation.v
parentadd6e85884691faef1bf8742e803374815672cc2 (diff)
correct and improve signature and documentation of FieldMixin
Documentation of FieldUnitMixin and FieldMixin corrected to reflect actual arguments, with mulVf and inv0 made explicit arguments for FieldMixin (they were implicit due to the extended signature of Field.mixin_of). Type of FieldMixin changed to a convertible variant to facilitate construction of on-the-fly in-proof construction of fieldType instances, exposing an idomainType instance.
Diffstat (limited to 'mathcomp/character/mxrepresentation.v')
0 files changed, 0 insertions, 0 deletions