Skip to content
CI

use coq.coercion.class as the type of coercion classes #480

Sign in to view logs

use coq.coercion.class as the type of coercion classes

use coq.coercion.class as the type of coercion classes #480

Triggered via pull request October 17, 2025 13:05
@garesgares
synchronize #909
coercion-class
Status Success
Total duration 7m 2s
Artifacts –

ci.yml

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

Annotations

50 warnings
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: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_tactic.v#L633
x is already taken, Elpi will make a name up
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, 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:dev, 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_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.