Add compute-lite target #286
JasonGrossAnnotations
2 errors and 40 warnings
|
master (native)
Canceling since a higher priority waiting request for 'CI (Coq)-master (native)-docker-build-native-6829223475' exists
|
|
check-all
Process completed with exit code 1.
|
|
master (for Coq CI, native):
theories/Util/PArray.v#L206
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/PArray.v#L242
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L219
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L220
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L221
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L222
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L223
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L224
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L225
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (for Coq CI, native):
theories/Util/Classes/Morphisms/Dependent.v#L226
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/PArray.v#L206
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/PArray.v#L242
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L219
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L220
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L221
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L222
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L223
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L224
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
theories/Util/Classes/Morphisms/Dependent.v#L225
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
master (native):
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.
|