Skip to content
Docker CI

Merge pull request #23 from coq-community/function_scope #28

Sign in to view logs

Merge pull request #23 from coq-community/function_scope

Merge pull request #23 from coq-community/function_scope #28

Triggered via push December 8, 2023 15:36
@pi8027pi8027
pushed fc68cb0
master
Status Success
Total duration 2m 37s
Artifacts –

docker-action.yml

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

Annotations

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