Bump etc/coq-scripts from 7b54b75 to 857071d
#341
dependabot[bot]coq.yml
on: pull_request
Matrix: docker-build-native
Matrix: docker-build
Annotations
2 errors and 50 warnings
|
8.17
Not an inductive definition.
|
|
check-all
Process completed with exit code 1.
|
|
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/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 (native)-computed:
theories/Util/Classes/Morphisms/Dependent.v#L227
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native)-computed:
theories/Util/Classes/Morphisms/Dependent.v#L228
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
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.
|
|
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.
|
|
master
Notation Zmod is deprecated since 8.17.
|