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

(limited to 'mathcomp/test-suite')

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