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/test-suite/hierarchy_test.v | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'mathcomp/test-suite')

diff --git a/mathcomp/test-suite/hierarchy_test.v b/mathcomp/test-suite/hierarchy_test.v
index 0085018..10564b9 100644
--- a/mathcomp/test-suite/hierarchy_test.v
+++ b/mathcomp/test-suite/hierarchy_test.v
@@ -705,15 +705,15 @@ Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type.
 Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type.
 
 (* fix in countalg *)
-Fail Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
 
 (* fix in finalg *)
-Fail Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type.
-Fail Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type.
-Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
-- 
cgit v1.2.3