Skip to content

Port to Hierarchy Builder #25

Port to Hierarchy Builder

Port to Hierarchy Builder #25

Triggered via pull request December 7, 2023 16:45
Status Success
Total duration 2m 35s
Artifacts

docker-action.yml

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

Annotations

50 warnings
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.unpickle by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickle by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enumP by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enum by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.addNr by
build (mathcomp/mathcomp:2.1.0-coq-8.16): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.opp by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.unpickle by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickle by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enumP by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enum by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.addNr by
build (mathcomp/mathcomp:2.1.0-coq-8.17): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.opp by
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/spec.v#L18
Hiding binding of key N to N_scope
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/spec/properties.v#L9
Hiding binding of key N to N_scope
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.unpickle by
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickle by
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enumP by
build (mathcomp/mathcomp:2.1.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enum by
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/spec.v#L18
Hiding binding of key N to N_scope
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/spec/properties.v#L9
Hiding binding of key N to N_scope
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.unpickle by
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickle by
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enumP by
build (mathcomp/mathcomp:2.0.0-coq-8.18): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enum by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.unpickle by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to isCountable.pickle by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enumP by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1975
Ignoring canonical projection to FinTuple.enum by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.addNr by
build (mathcomp/mathcomp:2.0.0-coq-8.16): src/spec/operations/properties.v#L1976
Ignoring canonical projection to GRing.isZmodule.opp by