Skip to content
Docker CI

fix some intuition and arith deprecations #9

Sign in to view logs

fix some intuition and arith deprecations

fix some intuition and arith deprecations #9

Triggered via pull request November 19, 2023 14:59
@palmskogpalmskog
opened #7
fix-deprec
Status Failure
Total duration 3m 1s
Artifacts –

docker-action.yml

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

Annotations

6 errors and 40 warnings
build (coqorg/coq:8.13): Arith/Nk_ind.v#L139
The reference Nat.add_0_r was not found in the current environment.
build (coqorg/coq:8.14): Arith/Nk_ind.v#L139
The reference Nat.add_0_r was not found in the current environment.
build (coqorg/coq:8.11): Arith/Nk_ind.v#L139
The reference Nat.add_0_r was not found in the current environment.
build (coqorg/coq:8.12): Arith/Nk_ind.v#L139
The reference Nat.add_0_r was not found in the current environment.
build (coqorg/coq:8.15): Arith/Nk_ind.v#L139
The reference Nat.add_0_r was not found in the current environment.
build (coqorg/coq:8.16): Arith/Znumfacts.v#L194
The reference extgcd was not found in the current environment.
build (coqorg/coq:8.16): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.16): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.16): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.16): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.16): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.16): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.16): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.16): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.16): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.16): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.18): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.18): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.18): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.18): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.18): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.17): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:8.17): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.17): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.17): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:8.17): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:dev): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:dev): Arith/Ninductions.v#L22
Notation le_n_Sn is deprecated since 8.16.
build (coqorg/coq:dev): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:dev): Arith/PI.v#L31
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:dev): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:dev): Arith/PI.v#L37
Notation le_Sn_n is deprecated since 8.16.
build (coqorg/coq:dev): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:dev): Reals/Rsequence/Rsequence_base_facts.v#L181
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:dev): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.
build (coqorg/coq:dev): Reals/Rsequence/Rsequence_base_facts.v#L196
Notation lt_n_Sm_le is deprecated since 8.16.