Skip to content
CI

Adapt to rocq#21180 #481

Sign in to view logs

Adapt to rocq#21180

Adapt to rocq#21180 #481

Triggered via pull request October 17, 2025 14:28
@TragicusTragicus
synchronize #907
Tragicus:rocq21180
Status Success
Total duration 5m 54s
Artifacts –

ci.yml

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

Annotations

50 warnings
docker (coqorg/coq:8.20, fatalwarnings): tests/test_arg_HOAS.v#L283
Automatically putting X1 in Prop even though it was declared with
docker (coqorg/coq:8.20, fatalwarnings): tests/test_File3.v#L18
This command does not support this attribute: phase.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L647
This command does not support this attribute: unknown.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L646
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L614
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L647
This command does not support this attribute: unknown.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L646
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, fatalwarnings): examples/tutorial_coq_elpi_command.v#L614
This command does not support these attributes: more, this.
docker (rocq/rocq-prover:9.1, dev): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (rocq/rocq-prover:9.1, dev): examples/tutorial_coq_elpi_HOAS.v#L420
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:9.1, dev): examples/tutorial_coq_elpi_HOAS.v#L419
Coq.Init.Datatypes.nat has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Datatypes.false has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Datatypes.true has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Datatypes.andb has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Datatypes.bool has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Logic.eq_refl has been replaced by
docker (rocq/rocq-prover:9.1, dev)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:9.0, dev): examples/tutorial_coq_elpi_command.v#L614
This command does not support these attributes: more, this.
docker (rocq/rocq-prover:9.0, dev): examples/tutorial_coq_elpi_HOAS.v#L420
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:9.0, dev): examples/tutorial_coq_elpi_HOAS.v#L419
Coq.Init.Datatypes.nat has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Datatypes.false has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Datatypes.true has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Datatypes.andb has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Datatypes.bool has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Logic.eq_refl has been replaced by
docker (rocq/rocq-prover:9.0, dev)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (coqorg/coq:8.20, dev): tests/test_arg_HOAS.v#L283
Automatically putting X1 in Prop even though it was declared with
docker (coqorg/coq:8.20, dev): tests/test_File3.v#L18
This command does not support this attribute: phase.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L647
This command does not support this attribute: unknown.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L646
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L614
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L647
This command does not support this attribute: unknown.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L646
This command does not support these attributes: more, this.
docker (coqorg/coq:8.20, dev): examples/tutorial_coq_elpi_command.v#L614
This command does not support these attributes: more, this.
docker (rocq/rocq-prover:dev, dev): examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
docker (rocq/rocq-prover:dev, dev): examples/tutorial_coq_elpi_HOAS.v#L420
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (rocq/rocq-prover:dev, dev): examples/tutorial_coq_elpi_HOAS.v#L419
Coq.Init.Datatypes.nat has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Datatypes.false has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Datatypes.true has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Datatypes.andb has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Datatypes.bool has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Logic.eq_refl has been replaced by
docker (rocq/rocq-prover:dev, dev)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.