Skip to content

Merge branch '8.20' into coq-master #435

Merge branch '8.20' into coq-master

Merge branch '8.20' into coq-master #435

Triggered via push January 6, 2025 19:23
Status Failure
Total duration 2m 17s
Artifacts

build.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

11 warnings
build
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build: theories/Chains/Inequalities.v#L19
Loading Stdlib without prefix is deprecated.
build: theories/Libs/Logic/InformativeEpsilon.v#L19
Loading Stdlib without prefix is deprecated.
build: theories/Notations/Sets.v#L19
Loading Stdlib without prefix is deprecated.
build: theories/Notations/Sets.v#L81
"From Coq" has been replaced by "From Stdlib".
build: theories/Notations/Reals.v#L19
"From Coq" has been replaced by "From Stdlib".
build: theories/Notations/Reals.v#L20
Loading Stdlib without prefix is deprecated.
build: tests/Notations/Sets.v#L41
"From Coq" has been replaced by "From Stdlib".
build: theories/Libs/Reals.v#L19
Loading Stdlib without prefix is deprecated.
build: theories/Libs/Reals.v#L20
"From Coq" has been replaced by "From Stdlib".
build: theories/Libs/Reals.v#L21
Loading Stdlib without prefix is deprecated.