Better HB structure #8
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
|