Skip to content

Adapt w.r.t. coq/coq#19228. (#62) #353

Adapt w.r.t. coq/coq#19228. (#62)

Adapt w.r.t. coq/coq#19228. (#62) #353

Triggered via pull request July 27, 2024 23:04
Status Failure
Total duration 20m 41s
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

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/Program/Basics/Dependent.v#L100
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
master (for Coq CI, native)-coq-ci-target: theories/Util/PArray.v#L164
Notations "_ .[ _ ]" defined at level 2 with arguments constr
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 (native)-computed-lite: theories/Util/Program/Basics/Dependent.v#L100
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
master (native)-computed-lite: theories/Util/Tactics2/List.v#L4
Unused variable: overlap.
master (native)-computed-lite: theories/Util/PArray.v#L164
Notations "_ .[ _ ]" defined at level 2 with arguments constr
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: theories/Util/Program/Basics/Dependent.v#L100
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
master (native)-computed: theories/Util/Tactics2/List.v#L4
Unused variable: overlap.
master (native)-computed: theories/Util/Program/PrimitiveBasics/Dependent.v#L2
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
master (native)-computed: theories/Util/PArray.v#L164
Notations "_ .[ _ ]" defined at level 2 with arguments constr
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
Notations "_ <| _ ; _ ; .. ; _ ::= _ |>" defined at level 12
master
Notations "_ <| _ ; _ ; .. ; _ ::= _ |>" defined at level 12
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.