Skip to content

remane gaussInteger -> gaussInt #7

remane gaussInteger -> gaussInt

remane gaussInteger -> gaussInt #7

Triggered via push October 27, 2023 09:24
Status Success
Total duration 3m 24s
Artifacts
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L203
Ignoring canonical projection to proj1 by GRing.isMul1Closed.rpred1
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L203
Ignoring canonical projection to proj2 by GRing.isMul2Closed.rpredM
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L203
Ignoring canonical projection to GRing.zmod_closedN by
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L203
Ignoring canonical projection to GRing.zmod_closedD by
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L226
Projection value has no head constant:
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L226
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L247
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L247
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L248
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L248
Ignoring canonical projection to eq_op by hasDecEq.eq_op in