Skip to content
CI

[derive.param1] Add some missing universe constraints #56

Sign in to view logs

[derive.param1] Add some missing universe constraints

[derive.param1] Add some missing universe constraints #56

Triggered via pull request January 28, 2025 13:48
@proux01proux01
opened #759
proux01:param1-add-typecheck
Status Success
Total duration 5m 39s
Artifacts –

ci.yml

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

Annotations

14 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 (coqorg/coq:dev)
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev)
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev)
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev)
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev): apps/derive/theories/derive/eqb_core_defs.v#L1
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev): apps/derive/theories/derive/eqb_core_defs.v#L2
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev)
Loading Stdlib without prefix is deprecated.
docker (coqorg/coq:dev)
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
docker (coqorg/coq:dev)
Coq.Init.Logic.eq_refl has been replaced by
docker (coqorg/coq:dev)
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.