Skip to content
Docker CI

Remove Stdlib dependency #213

Sign in to view logs

Remove Stdlib dependency

Remove Stdlib dependency #213

Triggered via pull request February 24, 2025 07:28
@proux01proux01
synchronize #97
proux01:no-stdlib
Status Success
Total duration 17m 46s
Artifacts –

docker-action.yml

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

Annotations

28 warnings
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L164
HB: no new instance is generated
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L252
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L259
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L301
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L318
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L325
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.19): theories/xmathcomp/various.v#L329
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/xmathcomp/real_closed_ext.v#L42
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1326
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1328
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.2.0-coq-8.19): theories/abel.v#L1330
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/real_closed_ext.v#L42
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L906
p_neq0 is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L911
ratr_p' is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L921
rp'_uniq is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L930
rp_perm is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L931
rp_uniq is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L936
ratr_p is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L950
K_eq is declared opaque (Qed) but this is not fully respected inside
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L953
K_split_p is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/abel.v#L959
p_sep is declared opaque (Qed) but this is not fully respected
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/real_closed_ext.v#L42
Notation rolle is deprecated since mathcomp-real-closed 2.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/abel.v#L1326
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/abel.v#L1328
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/abel.v#L1330
Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.