From 7ab5c99ab4c2ecfd55702a4279392f067652e357 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 3 Apr 2019 10:01:50 +0200
Subject: Fix inheritances in ssrnum

---
 mathcomp/algebra/ssrnum.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra')

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.
-- 
cgit v1.2.3