Skip to content
Docker CI

fix some intuition and arith deprecations #12

Sign in to view logs

fix some intuition and arith deprecations

fix some intuition and arith deprecations #12

Triggered via pull request December 3, 2023 14:51
@palmskogpalmskog
synchronize #7
fix-deprec
Status Failure
Total duration 2m 57s
Artifacts –

docker-action.yml

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

Annotations

1 error and 20 warnings
build (coqorg/coq:dev): Arith/Nk_ind.v#L22
Cannot find a physical path bound to logical path Plus.
build (coqorg/coq:8.17): Reals/Rtactic.v#L544
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L40
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L48
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L57
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L62
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L67
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L72
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L82
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L91
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.17): Hierarchy/Type_class_definition.v#L96
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Reals/RFsequence.v#L27
Hiding binding of key Rseq to Rseq_scope
build (coqorg/coq:8.18): Reals/Rtactic.v#L544
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L40
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L48
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L57
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L62
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L67
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L72
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L82
A coercion will be introduced instead of an instance in future
build (coqorg/coq:8.18): Hierarchy/Type_class_definition.v#L91
A coercion will be introduced instead of an instance in future