diff options
| author | Kazuhiko Sakaguchi | 2019-04-03 10:01:50 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-04-03 10:01:50 +0200 |
| commit | 7ab5c99ab4c2ecfd55702a4279392f067652e357 (patch) | |
| tree | ce2a485f9f5db110a4a4d79b097158c921f84a01 /mathcomp/algebra | |
| parent | fa01cdf52c9af3f7e57a865a063e3d02f28cbf60 (diff) | |
Fix inheritances in ssrnum
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 5e33c7f..a1975ff 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -419,6 +419,7 @@ Coercion numDomainType : type >-> NumDomain.type. Canonical numDomainType. Coercion fieldType : type >-> GRing.Field.type. Canonical fieldType. +Canonical join_numDomainType. Notation numFieldType := type. Notation "[ 'numFieldType' 'of' T ]" := (@pack T _ _ id _ _ id) (at level 0, format "[ 'numFieldType' 'of' T ]") : form_scope. @@ -627,7 +628,8 @@ Definition numDomainType := @NumDomain.Pack cT xclass. Definition realDomainType := @RealDomain.Pack cT xclass. Definition fieldType := @GRing.Field.Pack cT xclass. Definition numFieldType := @NumField.Pack cT xclass. -Definition join_realDomainType := @RealDomain.Pack numFieldType xclass. +Definition join_fieldType := @GRing.Field.Pack realDomainType xclass. +Definition join_numFieldType := @NumField.Pack realDomainType xclass. End ClassDef. @@ -660,7 +662,8 @@ Coercion fieldType : type >-> GRing.Field.type. Canonical fieldType. Coercion numFieldType : type >-> NumField.type. Canonical numFieldType. -Canonical join_realDomainType. +Canonical join_fieldType. +Canonical join_numFieldType. Notation realFieldType := type. Notation "[ 'realFieldType' 'of' T ]" := (@pack T _ _ id _ _ id) (at level 0, format "[ 'realFieldType' 'of' T ]") : form_scope. |