Could not find a terminator for warning: File "./theories/Classes/implementations/binary_naturals.v", line 71, characters 2-6: Warning: succunary is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

succunary is declared opaque (Qed) but this is not fully respected

Could not find a terminator for warning: File "./theories/Classes/implementations/binary_naturals.v", line 78, characters 2-6: Warning: unarybinary is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

unarybinary is declared opaque (Qed) but this is not fully respected

Could not find a terminator for warning: File "./theories/Classes/implementations/binary_naturals.v", line 102, characters 2-6: Warning: binaryunary is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

binaryunary is declared opaque (Qed) but this is not fully respected

Could not find a terminator for warning: File "./theories/Classes/implementations/binary_naturals.v", line 425, characters 24-28: Warning: f_preserves_0 is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

f_preserves_0 is declared opaque (Qed) but this is not fully

Could not find a terminator for warning: File "./theories/Classes/implementations/binary_naturals.v", line 431, characters 4-8: Warning: f_preserves_1 is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]