use coq.coercion.class as the type of coercion classes #479
Annotations
10 warnings
|
Run coq-community/docker-coq-action@v1:
examples/tutorial_coq_elpi_tactic.v#L633
x is already taken, Elpi will make a name up
|
|
Run coq-community/docker-coq-action@v1:
examples/tutorial_coq_elpi_HOAS.v#L420
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
|
|
Run coq-community/docker-coq-action@v1:
examples/tutorial_coq_elpi_HOAS.v#L419
Coq.Init.Datatypes.nat has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Datatypes.false has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Datatypes.true has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Datatypes.andb has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Datatypes.bool has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Logic.False has been replaced by Corelib.Init.Logic.False.
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Logic.eq_refl has been replaced by
|
|
Run coq-community/docker-coq-action@v1
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
|
Loading