Skip to content
CI

CI #1087

Sign in to view logs

CI

CI #1087

Triggered via schedule September 8, 2025 05:23
@proux01proux01
⁠ b4f4005
master
Status Failure
Total duration 10m 15s
Artifacts –

coq-action.yml

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

Annotations

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