Skip to content

Change implementation of lsr #113

Change implementation of lsr

Change implementation of lsr #113

Triggered via push May 23, 2024 07:13
Status Success
Total duration 4m 43s
Artifacts

ci.yml

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

Annotations

114 warnings
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.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.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.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.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.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.
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.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.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.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.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