From fa01cdf52c9af3f7e57a865a063e3d02f28cbf60 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 2 Apr 2019 20:34:01 +0200
Subject: Fix inheritances in countalg and finalg (the 2nd attempt)

---
 mathcomp/algebra/countalg.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'mathcomp/algebra/countalg.v')

diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v
index f82a231..962a296 100644
--- a/mathcomp/algebra/countalg.v
+++ b/mathcomp/algebra/countalg.v
@@ -762,6 +762,8 @@ Coercion countComUnitRingType : type >-> ComUnitRing.type.
 Canonical countComUnitRingType.
 Coercion idomainType : type >-> GRing.IntegralDomain.type.
 Canonical idomainType.
+Coercion countIdomainType : type >-> IntegralDomain.type.
+Canonical countIdomainType.
 Coercion fieldType : type >-> GRing.Field.type.
 Canonical fieldType.
 Coercion countFieldType : type >-> Field.type.
@@ -794,4 +796,4 @@ End CountRing.
 Import CountRing.
 Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports.
 Export ComUnitRing.Exports IntegralDomain.Exports.
-Export Field.Exports DecidableField.Exports ClosedField.Exports.
\ No newline at end of file
+Export Field.Exports DecidableField.Exports ClosedField.Exports.
-- 
cgit v1.2.3