Adapt w.r.t. coq/coq#19228. #349
JasonGrosscoq.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/Program/Basics/Dependent.v#L100
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Tactics2/List.v#L4
Unused variable: overlap.
|
|
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.
|