Skip to content
Docker CI

Merge pull request #53 from thery/rocq #304

Sign in to view logs

Merge pull request #53 from thery/rocq

Merge pull request #53 from thery/rocq #304

Triggered via push October 31, 2025 10:48
@therythery
pushed cc7d4cc
master
Status Success
Total duration 2m 20s
Artifacts –

docker-action.yml

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

Annotations

21 warnings
build (rocq/rocq-prover:dev): theories/Frequency.v#L35
Notation Permutation_app_swap is deprecated since 9.1.
build (rocq/rocq-prover:dev): theories/ISort.v#L38
Notation Permutation_app_swap is deprecated since 9.1.
build (rocq/rocq-prover:dev): theories/Frequency.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/ISort.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/UniqueKey.v#L34
Notation Permutation_app_swap is deprecated since 9.1.
build (rocq/rocq-prover:dev): theories/UniqueKey.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/Ordered.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/AuxLib.v#L460
Notation Permutation_app_swap is deprecated since 9.1.
build (rocq/rocq-prover:dev): theories/AuxLib.v#L24
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:dev): theories/AuxLib.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Weight.v#L63
Notation app_length is deprecated since 8.20.
build (rocq/rocq-prover:9.0): theories/Weight.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Code.v#L25
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Code.v#L24
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Frequency.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/ISort.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/UniqueKey.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/Ordered.v#L23
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/AuxLib.v#L24
"From Coq" has been replaced by "From Stdlib".
build (rocq/rocq-prover:9.0): theories/AuxLib.v#L23
"From Coq" has been replaced by "From Stdlib".
build (coqorg/coq:8.19): src/Extraction.v#L35
Setting extraction output directory by default to