Skip to content
CI

CI #1226

Sign in to view logs

CI

CI #1226

Triggered via schedule January 17, 2026 05:26
@proux01proux01
⁠ e170ac0
master
Status Success
Total duration 10m 33s
Artifacts –

coq-action.yml

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

Annotations

30 warnings
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L268
Reference Frobenius_autE is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L268
Reference Frobenius_autE is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection2.v#L262
Notation "[ char _ ]" is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1): theories/BGsection1.v#L102
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/BGsection2.v#L195
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/BGsection2.v#L194
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/BGsection2.v#L193
Use of "Notation" keyword for abbreviations is deprecated, use
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/PFsection1.v#L694
Use of "Notation" keyword for abbreviations is deprecated, use
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#L839
Notation expgn is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/PFsection1.v#L38
Notation invg is deprecated since mathcomp 2.5.0. Use inv instead.
build (mathcomp/mathcomp-dev:rocq-prover-dev): theories/BGsection1.v#L102
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection2.v#L267
Notation Frobenius_aut is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection2.v#L262
Notation "[ char _ ]" is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/PFsection1.v#L540
Notation truncK is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/PFsection1.v#L38
Notation invg is deprecated since mathcomp 2.5.0. Use inv instead.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection1.v#L839
Notation expgn is deprecated since mathcomp 2.5.0.
build (mathcomp/mathcomp-dev:rocq-prover-9.1): theories/BGsection1.v#L102
Notation nosimpl is deprecated since mathcomp 2.3.0.