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 | |
| parent | fa01cdf52c9af3f7e57a865a063e3d02f28cbf60 (diff) | |
Fix inheritances in ssrnum
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 7 | ||||
| -rw-r--r-- | mathcomp/test-suite/hierarchy_test.v | 4 |
2 files changed, 7 insertions, 4 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. diff --git a/mathcomp/test-suite/hierarchy_test.v b/mathcomp/test-suite/hierarchy_test.v index 10564b9..a2bbf37 100644 --- a/mathcomp/test-suite/hierarchy_test.v +++ b/mathcomp/test-suite/hierarchy_test.v @@ -701,8 +701,8 @@ Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Typ Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type. (* fix in ssrnum *) -Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type. -Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type. (* fix in countalg *) Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type. |