diff options
| author | Kazuhiko Sakaguchi | 2019-04-03 10:01:50 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-04-03 10:01:50 +0200 |
| commit | 7ab5c99ab4c2ecfd55702a4279392f067652e357 (patch) | |
| tree | ce2a485f9f5db110a4a4d79b097158c921f84a01 /mathcomp/test-suite/hierarchy_test.v | |
| parent | fa01cdf52c9af3f7e57a865a063e3d02f28cbf60 (diff) | |
Fix inheritances in ssrnum
Diffstat (limited to 'mathcomp/test-suite/hierarchy_test.v')
| -rw-r--r-- | mathcomp/test-suite/hierarchy_test.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |