Skip to content

Bump etc/coq-scripts from d3dc888 to 7b54b75 #323

Bump etc/coq-scripts from d3dc888 to 7b54b75

Bump etc/coq-scripts from d3dc888 to 7b54b75 #323

Triggered via pull request December 25, 2023 07:55
Status Success
Total duration 1h 21m 0s
Artifacts

coq.yml

on: pull_request
Matrix: docker-build-native
Matrix: docker-build
check-all
0s
check-all
Update tested
0s
Update tested
Fit to window
Zoom out
Zoom in

Annotations

50 warnings
master (for Coq CI, native)-coq-ci-target: theories/Util/PArray.v#L206
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/PArray.v#L242
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L219
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L220
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L221
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L222
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L223
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L224
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L225
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (for Coq CI, native)-coq-ci-target: theories/Util/Classes/Morphisms/Dependent.v#L226
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/PArray.v#L206
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/PArray.v#L242
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L219
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L220
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L221
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L222
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L223
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L224
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L225
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed-lite: theories/Util/Classes/Morphisms/Dependent.v#L226
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/PArray.v#L206
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/PArray.v#L242
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L219
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L220
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L221
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L222
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L223
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L224
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L225
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master (native)-computed: theories/Util/Classes/Morphisms/Dependent.v#L226
The '%' scope delimiter in 'Arguments' commands is deprecated, use
master
Unused variable Empty_string might be a misspelled constructor. Use
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
master
Notation Zmod is deprecated since 8.17.
8.17
Notation "[ predI _ & _ ]" was already used in scope fun_scope.
8.17
Notation "[ predU _ & _ ]" was already used in scope fun_scope.
8.17
Notation "[ predD _ & _ ]" was already used in scope fun_scope.
8.17
Notation "[ predC _ ]" was already used in scope fun_scope.
8.17
Notation "[ preim _ of _ ]" was already used in scope fun_scope.
8.17
Notation "_ + _" was already used in scope nat_scope.
8.17
Notation "_ - _" was already used in scope nat_scope.
8.17
Notation "_ <= _" was already used in scope nat_scope.
8.17
Notation "_ < _" was already used in scope nat_scope.
8.17
Notation "_ >= _" was already used in scope nat_scope.