Bump regex from 2022.7.9 to 2023.10.3 in /training #278
dependabot[bot]coq.yml
on: pull_request
Matrix: docker-build-native
Matrix: docker-build
Annotations
30 warnings
|
master (native):
theories/MaxOfTwoNumbersSimpler/Computed/AllMaskedAttnScores.v#L12
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllAttnPattern.v#L12
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbersSimpler/Computed/AllMaskedAttnScores.v#L14
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllLogits.v#L8
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllAttnPattern.v#L14
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllMaskedAttnScores.v#L12
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllMaskedAttnScores.v#L14
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbers/Computed/AllLogits.v#L10
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbersSimpler/Computed/AllAttnPattern.v#L12
This command does not support this attribute: native_compile.
|
|
master (native):
theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v#L8
This command does not support this attribute: native_compile.
|
|
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.
|