diff options
| author | Kazuhiko Sakaguchi | 2019-04-02 20:34:01 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-04-02 20:34:01 +0200 |
| commit | fa01cdf52c9af3f7e57a865a063e3d02f28cbf60 (patch) | |
| tree | 1fab6add707d8bddb48424f84a00fef95e7e1dc8 /mathcomp/test-suite | |
| parent | beb5b00f4f35859f48f12a6e0dd9e86d65609822 (diff) | |
Fix inheritances in countalg and finalg (the 2nd attempt)
Diffstat (limited to 'mathcomp/test-suite')
| -rw-r--r-- | mathcomp/test-suite/hierarchy_test.v | 20 |
1 files changed, 10 insertions, 10 deletions
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. |