Skip to content

Port to hierarchy builder #177

Port to hierarchy builder

Port to hierarchy builder #177

Triggered via pull request November 6, 2023 16:09
Status Success
Total duration 43m 7s
Artifacts

docker-action.yml

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

Annotations

70 warnings
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.18): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-dev): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.17): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp-dev:coq-8.16): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/char0.v#L115
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/cyclotomic_ext.v#L160
Notation rmorphX is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): theories/xmathcomp/algR.v#L38
Notation ler_norm_add is deprecated since mathcomp 1.17.0.