Skip to content
Docker CI

fix compute #9

Sign in to view logs

fix compute

fix compute #9

Triggered via push October 29, 2023 01:50
@therythery
pushed cf031a5
master
Status Success
Total duration 3m 21s
Artifacts –
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

docker-action.yml

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

Annotations

10 warnings
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L74
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L98
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section4.v#L108
Not a truly recursive fixpoint.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L21
Ignoring canonical projection to cons by isFinite.enum_subdef in
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L82
Notation UniqFinMixin is deprecated since mathcomp 2.0.0.
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Projection value has no head constant:
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L375
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L378
Projection value has no head constant:
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L378
Ignoring canonical projection to vrefl_rect by isSub.SubK_subproof
build (mathcomp/mathcomp:2.1.0-coq-8.18): AnIntroductionToSmallScaleReflectionInCoq/section6.v#L389
Ignoring canonical projection to cat by tval in cat_tuple: redundant