Skip to content
Docker CI

fix some intuition and arith deprecations #10

Sign in to view logs

fix some intuition and arith deprecations

fix some intuition and arith deprecations #10

Triggered via pull request November 19, 2023 15:06
@palmskogpalmskog
synchronize #7
fix-deprec
Status Success
Total duration 2m 58s
Artifacts –

docker-action.yml

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

Annotations

30 warnings
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.