Skip to content
.github/workflows/ci.yml

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

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 #127

Triggered via pull request February 26, 2026 08:09
@proux01proux01
opened #36
proux01:mc1545
Status Success
Total duration 31m 24s
Artifacts –

ci.yml

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

Annotations

47 warnings
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L474
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L474
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0): src/word_ssrZ.v#L26
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word.v#L474
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word_ssrZ.v#L114
Notation GRing.ComRing_hasMulInverse.Build is deprecated
build (mathcomp/mathcomp:2.4.0-coq-8.20): src/word_ssrZ.v#L92
Notation GRing.Zmodule_isComRing.Build is deprecated
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1051
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1008
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L599
Notation nosimpl is deprecated since mathcomp 2.3.0.