Skip to content
CI

Adapt to https://github.com/coq/coq/pull/19519 #192

Sign in to view logs

Adapt to https://github.com/coq/coq/pull/19519

Adapt to https://github.com/coq/coq/pull/19519 #192

Triggered via pull request September 10, 2024 12:11
@proux01proux01
opened #114
proux01:coq_19519
Status Failure
Total duration 50m 42s
Artifacts –

ci.yml

on: pull_request
check-goose
44s
check-goose
python
16s
python
Matrix: build-vos
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

6 errors and 20 warnings
build-vos (dev): src/program_proof/vrsm/storage/proof.v#L260
The following term contains unresolved implicit arguments:
build-vos (dev): src/program_proof/jrnl/sep_jrnl_invariant.v#L73
The following term contains unresolved implicit arguments:
build (dev): src/program_proof/jrnl/sep_jrnl_invariant.v#L73
The following term contains unresolved implicit arguments:
build (dev): src/program_proof/vrsm/storage/proof.v#L260
The following term contains unresolved implicit arguments:
build (8.19): src/program_proof/jrnl/sep_jrnl_invariant.v#L73
The following term contains unresolved implicit arguments:
build (8.19): src/program_proof/vrsm/storage/proof.v#L260
The following term contains unresolved implicit arguments:
build-vos (dev): external/coqutil/src/coqutil/Z/Lia.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
build-vos (dev): external/coqutil/src/coqutil/Z/div_mod_to_equations.v#L1
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
build-vos (dev): external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinIntDef has been replaced by Stdlib.ZArith.BinIntDef.
build-vos (dev): external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
build-vos (dev): external/coqutil/src/coqutil/Z/Lia.v#L2
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
build-vos (dev): external/coqutil/src/coqutil/Z/PushPullMod.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
build-vos (dev): external/coqutil/src/coqutil/Sorting/Permutation.v#L1
Coq.Sorting.Permutation has been replaced by Stdlib.Sorting.Permutation.
build-vos (dev): external/stdpp/stdpp/base.v#L11
"From Coq" has been replaced by "From Stdlib".
build-vos (dev): external/stdpp/stdpp/base.v#L12
"From Coq" has been replaced by "From Stdlib".
build-vos (dev): external/stdpp/stdpp/base.v#L14
Coq.Program has been replaced by Stdlib.Program.
build (dev): external/coqutil/src/coqutil/Z/Lia.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
build (dev): external/coqutil/src/coqutil/Z/div_mod_to_equations.v#L1
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
build (dev): external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinIntDef has been replaced by Stdlib.ZArith.BinIntDef.
build (dev): external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
build (dev): external/coqutil/src/coqutil/Z/Lia.v#L2
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
build (dev): external/coqutil/src/coqutil/Z/PushPullMod.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
build (dev): external/coqutil/src/coqutil/Sorting/Permutation.v#L1
Coq.Sorting.Permutation has been replaced by Stdlib.Sorting.Permutation.
build (dev): external/stdpp/stdpp/base.v#L11
"From Coq" has been replaced by "From Stdlib".
build (dev): external/stdpp/stdpp/base.v#L12
"From Coq" has been replaced by "From Stdlib".
build (dev): external/stdpp/stdpp/base.v#L14
Coq.Program has been replaced by Stdlib.Program.