Skip to content
Docker CI

Adapt to https://github.com/math-comp/math-comp/pull/1545 #372

Sign in to view logs

Adapt to https://github.com/math-comp/math-comp/pull/1545

Adapt to https://github.com/math-comp/math-comp/pull/1545 #372

Triggered via pull request February 26, 2026 14:27
@proux01proux01
synchronize #129
proux01:mc1545
Status Failure
Total duration 12m 20s
Artifacts –

docker-action.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

40 warnings
build (mathcomp/mathcomp-dev:rocq-prover-9.0): examples/field_examples_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): examples/field_examples_no_check.v#L1
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/lra.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/lra.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/ring.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L1336
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L1336
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L5
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-9.0): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L1073
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L765
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L762
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L561
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L558
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L390
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L388
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L5
Library File mathcomp.ssreflect.all_ssreflect is deprecated
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0)
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/lra.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/ring.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/lra.v#L3
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L1336
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L1336
Reference Zeq_is_eq_bool is deprecated since 9.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L4
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): theories/common.v#L3
"From Coq" has been replaced by "From Stdlib".