diff options
| author | Georges Gonthier | 2018-11-26 19:51:27 +0100 |
|---|---|---|
| committer | Georges Gonthier | 2018-11-26 19:51:27 +0100 |
| commit | 03ad994dfee48e1a7b2b7091c45dfdcf4402f826 (patch) | |
| tree | d891c2b8507452f2aaac1cbfe7dfbb709e751629 /mathcomp/field/algC.v | |
| parent | add6e85884691faef1bf8742e803374815672cc2 (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/field/algC.v')
| -rw-r--r-- | mathcomp/field/algC.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index aef136a..4b37a9c 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -377,7 +377,7 @@ Definition unitRingMixin := FieldUnitMixin mulVf inv0. Canonical unitRingType := UnitRingType type unitRingMixin. Canonical comUnitRingType := [comUnitRingType of type]. -Definition fieldMixin := @FieldMixin _ _ mulVf inv0. +Definition fieldMixin := FieldMixin mulVf inv0. Definition idomainAxiom := FieldIdomainMixin fieldMixin. Canonical idomainType := IdomainType type idomainAxiom. Canonical fieldType := FieldType type fieldMixin. |