Skip to content

removing obsolete templates (#30) #59

removing obsolete templates (#30)

removing obsolete templates (#30) #59

Triggered via push October 7, 2024 18:39
Status Success
Total duration 12m 40s
Artifacts
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