Skip to content
CI

CI #1044

Sign in to view logs

CI

CI #1044

Triggered via schedule July 31, 2025 05:33
@proux01proux01
⁠ ab32f3e
master
Status Failure
Total duration 40m 21s
Artifacts –

coq-action.yml

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

Annotations

10 warnings
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L268
Reference Frobenius_autE is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L268
Reference Frobenius_autE is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection2.v#L262
Notation "[ char _ ]" is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/BGsection1.v#L102
Notation nosimpl is deprecated since mathcomp 2.3.0.