Skip to content
Docker CI

make coq-htt package depend on coq-htt-core (#29) #57

Sign in to view logs

make coq-htt package depend on coq-htt-core (#29)

make coq-htt package depend on coq-htt-core (#29) #57

Triggered via push October 7, 2024 18:19
@aleksnanevskialeksnanevski
pushed 3daf5b9
master
Status Success
Total duration 12m 50s
Artifacts –

docker-action.yml

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

Annotations

17 warnings
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/array.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/quicksort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/bubblesort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/congmath.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/hashtab.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/union_find.v#L14
Notations "[ seq _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): examples/congprog.v#L16
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): htt/domain.v#L15
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/exploit.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/array.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/array.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): examples/gcd.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/kvmaps.v#L19
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/dlist.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/quicksort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:latest-coq-dev): examples/bubblesort.v#L14
"From Coq" has been replaced by "From Stdlib".
build (mathcomp/mathcomp:latest-coq-dev): examples/bubblesort.v#L15
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments