Skip to content
.github/workflows/ci.yml

Do not require all_algebra #97

Sign in to view logs

Do not require all_algebra

Do not require all_algebra #97

Triggered via push March 21, 2024 05:58
@vbglvbgl
pushed f42c6c8
2.x-less-algebra
Status Success
Total duration 1h 35m 51s
Artifacts –

ci.yml

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

Annotations

114 warnings
build (mathcomp/mathcomp:1.16.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.16.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.16.0-coq-8.18): src/word.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.16.0-coq-8.18): src/word.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.17): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.16): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.17.0-coq-8.18): src/word.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.17): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.18.0-coq-8.18): src/word.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.17): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.17.0-coq-8.15): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.19.0-coq-8.18): src/word.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word.v#L25
Hiding binding of key N to nat_scope
build (mathcomp/mathcomp:1.19.0-coq-8.19): src/word.v#L25
Hiding binding of key Z to int_scope
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.18.0-coq-8.16): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L314
Notation ler_oppr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word_ssrZ.v#L337
Notation ltr_subl_addr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word.v#L379
Notation ler_pmulr is deprecated since mathcomp 1.17.0.
build (mathcomp/mathcomp:1.19.0-coq-8.16): src/word.v#L518
Notation ler_pemulr is deprecated since mathcomp 1.17.0.