Skip to content
.github/workflows/ci.yml

Remove lemmas addP and mulP #123

Sign in to view logs

Remove lemmas addP and mulP

Remove lemmas addP and mulP #123

Triggered via pull request November 6, 2025 05:24
@vbglvbgl
synchronize #35
vbgl:exit-addP
Status Success
Total duration 36m 18s
Artifacts –

ci.yml

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

Annotations

19 warnings
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1048
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L1007
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.20): src/word.v#L598
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "\pi ( _ )" defined at level 2 and "\pi"
build (mathcomp/mathcomp:2.2.0-coq-8.20): src/word_ssrZ.v#L25
Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1048
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L1007
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.19): src/word.v#L598
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1050
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1049
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1048
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L1007
Notation nosimpl is deprecated since mathcomp 2.3.0.
build (mathcomp/mathcomp:2.3.0-coq-8.18): src/word.v#L598
Notation nosimpl is deprecated since mathcomp 2.3.0.