Cleanup for overridden notations

[DmxLarchey]

This PR is a follow up of #231. It intends to solve remaining issues related to overridden notations, ie warnings that pop up when compiling without the flag -notation-overridden. @dominik-kirst would you mind having a look? Orelse pinging the author of the corresponding files? I also ping @mrhaandi who initiated those warning issues in the master branch.

Notice that this branch is supposed to be compiled with rocq, not coq.

The concerned files are below.

Proposed solutions by @DmxLarchey :

• FOL/FOL.v;
• FOL/Utils/FriedmanTranslation.v;
• FOL/Utils/FriedmanTranslationFragment.v;
• FOL/Reductions/H10p_to_FA.v.

Proposed solutions by @mrhaandi :

• FOL/binFST_undec.v;
• FOL/Semantics/FiniteTarski/DoubleNegation.v;
• FOL/Reductions/H10UPC_to_FOL_friedman.v;
• FOL/Reductions/binZF_to_binFST.v;
• FOL/Reductions/ZF_to_FST.v.

[mrhaandi]

DmxLarchey#16 corrects scoping issues in the Unsolved so far cases, leaving no warnings.

[mrhaandi]

The CI currently fails because rocq changed its package structure.

[DmxLarchey]

@dominik-kirst Could you please have a look at the proposed changes. They are all in the theories/FOL sub-dir and thus most likely code that you wrote yourself or participate in writing. Best, Dominique.

[mrhaandi]

@DmxLarchey could you integrate #236 into this PR?

[DmxLarchey]

@DmxLarchey could you integrate #236 into this PR?

Done

[JoJoDeveloping]

Apart from that, what is missing for this PR? I not really sure what is the difference between the two proposed solutions from the PR description.. Which is this, where can I find the other one?

[mrhaandi]

These are not alternatives per se, but the combination of two distinct solutions for different files. @DmxLarchey put notations in Modules (as should be standard). This did not work for other files, which were incorrectly scoped.

[DmxLarchey]

Apart from that, what is missing for this PR? I not really sure what is the difference between the two proposed solutions from the PR description.. Which is this, where can I find the other one?

Nothing really but I did propose @dominik-kirst for a review. But we can merge w/o that review.

[dominik-kirst]

Looks all good to me, sorry for the delay!

[mrhaandi]

@DmxLarchey with @dominik-kirst's approval if it is fine with you, I can merge now.

[DmxLarchey]

@DmxLarchey with @dominik-kirst's approval if it is fine with you, I can merge now.

Thanks for doing this.