Skip to content
CI

Fix #766 #87

Sign in to view logs

Fix #766

Fix #766 #87

Triggered via pull request February 6, 2025 15:37
@proux01proux01
opened #770
proux01:fix-766
Status Success
Total duration 5m 0s
Artifacts –

ci.yml

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

Annotations

24 warnings
docker (coqorg/coq:8.20): examples/tutorial_coq_elpi_command.v#L610
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20): examples/tutorial_coq_elpi_command.v#L643
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20): examples/tutorial_coq_elpi_command.v#L644
This command does not support this attribute: unknown.
docker (coqorg/coq:8.20): examples/tutorial_coq_elpi_tactic.v#L632
x is already taken, Elpi will make a name up
docker (rocq/rocq-prover:dev)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev): apps/derive/theories/derive/eqb_core_defs.v#L1
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev): apps/derive/theories/derive/eqb_core_defs.v#L2
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:dev)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:dev)
Coq.Init.Logic.eq_refl has been replaced by
docker (rocq/rocq-prover:dev)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.
docker (rocq/rocq-prover:9.0)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0): apps/derive/theories/derive/eqb_core_defs.v#L1
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0): apps/derive/theories/derive/eqb_core_defs.v#L2
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0)
Loading Stdlib without prefix is deprecated.
docker (rocq/rocq-prover:9.0)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:9.0)
Coq.Init.Logic.eq_refl has been replaced by
docker (rocq/rocq-prover:9.0)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.