Skip to content

Better HB structure

Better HB structure #8

Triggered via push November 2, 2023 12:46
Status Success
Total duration 3m 37s
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#L250
Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L250
Ignoring canonical projection to eq_op by hasDecEq.eq_op in
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L250
Ignoring canonical projection to isCountable.pickleK by
build (mathcomp/mathcomp:2.1.0-coq-8.18): gauss_int.v#L250
Ignoring canonical projection to isCountable.unpickle by