Skip to content

Port to hierarchy builder #175

Port to hierarchy builder

Port to hierarchy builder #175

Triggered via pull request November 6, 2023 12:31
Status Failure
Total duration 37m 10s
Artifacts

docker-action.yml

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

Annotations

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