Skip to content
Docker CI

Coq 8.20, rm infra.v, minor fixes #149

Sign in to view logs

Coq 8.20, rm infra.v, minor fixes

Coq 8.20, rm infra.v, minor fixes #149

Triggered via pull request February 19, 2025 14:45
@affeldt-aistaffeldt-aist
synchronize #38
fix_20250219
Status Failure
Total duration 26m 34s
Artifacts –

docker-action.yml

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

Annotations

1 error and 20 warnings
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/intersection.v#L310
The reference Order.TMeetTheory.meets_ge was not found in the current
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L446
Ignoring canonical projection to GRing.scalable_linear by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L446
Ignoring canonical projection to pair_of_and by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L446
Ignoring canonical projection to GRing.scalable_linear by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L446
Ignoring canonical projection to pair_of_and by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L511
Ignoring canonical projection to GRing.scalable_linear by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/pol.v#L511
Ignoring canonical projection to pair_of_and by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/desc2.v#L488
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/desc2.v#L488
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/three_circles.v#L157
Ignoring canonical projection to GRing.scalable_linear by
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/three_circles.v#L157
Ignoring canonical projection to pair_of_and by
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference addn_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference addn_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L56
Reference addn_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L83
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L83
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L83
Reference muln_rec is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): theories/preliminaries.v#L84
Reference muln_rec is deprecated since mathcomp 2.3.0.