Adapt to https://github.com/coq/coq/pull/19530 #355
JasonGrosscoq.yml
on: pull_request
Matrix: docker-build-native
Matrix: docker-build
Annotations
50 warnings
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Pointed.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Default.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Arith/ZArith.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Bool.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/List.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Program/Basics/Dependent.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
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/Compat/Arith/PeanoNat.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/Relations/Relation_Definitions/Hetero.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (for Coq CI, native)-coq-ci-target:
theories/Util/IffT.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
master (native)-computed-lite:
theories/Util/Default.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/Pointed.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/Arith/ZArith.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/Bool.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/List.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/Program/Basics/Dependent.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
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/Compat/Arith/PeanoNat.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/Relations/Relation_Definitions/Hetero.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed-lite:
theories/Util/IffT.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
master (native)-computed:
theories/Util/Default.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Pointed.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Arith/ZArith.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Bool.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/List.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Program/Basics/Dependent.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Program/Basics/Dependent.v#L100
Notations "∀ _ .. _ , _" defined at level 10 with arguments binder
|
|
master (native)-computed:
theories/Util/Relations/Relation_Definitions/Hetero.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/Compat/Arith/PeanoNat.v#L1
"From Coq" has been replaced by "From Stdlib".
|
|
master (native)-computed:
theories/Util/IffT.v#L1
Coq.Classes has been replaced by Stdlib.Classes.
|
|
master
Notations "_ <| _ ; _ ; .. ; _ ::= _ |>" defined at level 12
|
|
master
Notations "_ <| _ ; _ ; .. ; _ ::= _ |>" defined at level 12
|
|
master
"From Coq" has been replaced by "From Stdlib".
|
|
master
"From Coq" has been replaced by "From Stdlib".
|
|
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.
|