Fix inheritances in ssrnum

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.