Skip to content
Docker CI

Merge pull request #97 from proux01/no-stdlib #216

Sign in to view logs

Merge pull request #97 from proux01/no-stdlib

Merge pull request #97 from proux01/no-stdlib #216

Triggered via push February 24, 2025 17:57
@CohenCyrilCohenCyril
pushed 05b1b9a
master
Status Success
Total duration 7m 1s
Artifacts –

docker-action.yml

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

Annotations

44 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-dev:coq-8.20): theories/xmathcomp/various.v#L164
HB: no new instance is generated
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L252
Notation comRingType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L259
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L301
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L318
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L322
Notation size_opp is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): theories/xmathcomp/various.v#L325
Notation ringType is deprecated since mathcomp 2.4.0.
build (mathcomp/mathcomp-dev:coq-8.20): 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.2.0-coq-8.20): theories/xmathcomp/various.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/char0.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/various.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/char0.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/cyclotomic_ext.v#L1
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/cyclotomic_ext.v#L1
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/map_gal.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/map_gal.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/algR.v#L2
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): theories/xmathcomp/algR.v#L2
Notations "\pi ( _ )" defined at level 2 and "\pi"
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