Skip to content
Docker CI

Port to MathComp 2 #148

Sign in to view logs

Port to MathComp 2

Port to MathComp 2 #148

Triggered via pull request September 29, 2023 13:21
@pi8027pi8027
synchronize #16
hierarchy-builder
Status Success
Total duration 45m 55s
Artifacts –

docker-action.yml

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

Annotations

70 warnings
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.0.0-coq-8.17): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L48
Notation ltr_pmul2l is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L49
Notation ltr_pmul is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L62
Notation ler_pemull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L69
Notation ler_pimull is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/extra_mathcomp.v#L93
Notation ler_pexpn2r is deprecated since mathcomp 1.17.0.