Skip to content

Adapt to https://github.com/math-comp/math-comp/pull/1354 #994

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

Adapt to https://github.com/math-comp/math-comp/pull/1354 #994

Triggered via pull request February 28, 2025 12:14
@proux01proux01
opened #72
mc1354
Status Failure
Total duration 9m 38s
Artifacts

docker-action.yml

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

Annotations

4 errors and 30 warnings
build (mathcomp/mathcomp:2.3.0-coq-8.20)
Notation "_ %:R" is already defined at level 2 with arguments constr
build (mathcomp/mathcomp:2.2.0-coq-8.19)
Notation "_ %:R" is already defined at level 2 with arguments constr
build (mathcomp/mathcomp:2.1.0-coq-8.18)
Notation "_ %:R" is already defined at level 2 with arguments constr
build (mathcomp/mathcomp-dev:rocq-prover-dev)
Notation "_ %:R" is already defined at level 2 with arguments constr
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.3.0-coq-8.20)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp:2.2.0-coq-8.19)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev)
The '%' scope delimiter in 'Arguments' commands is deprecated, use