Drop back down to 1.17 for coq-mathcomp-analysis #273
JasonGrossAnnotations
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 minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation not_le_minus_0 is deprecated since 8.16.
|
|
8.17
Notation not_le_minus_0 is deprecated since 8.16.
|
|
8.17
Notation minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation minus_Sn_m is deprecated since 8.16.
|
|
8.17
Notation le_n_0_eq is deprecated since 8.16.
|
|
8.17
Notation le_plus_minus_r is deprecated since 8.16.
|