Skip to content

Port to hierarchy builder #176

Port to hierarchy builder

Port to hierarchy builder #176

Triggered via pull request November 6, 2023 15:30
Status Failure
Total duration 40m 32s
Artifacts

docker-action.yml

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

Annotations

30 warnings
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-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.