Dealing with -notation-overridden compile option

[DmxLarchey]

So far:

• the ILL/* sub-folders cleaned up by introducing Modules for notations;

Currently remaining, exhaustive list:

• FOL/FOL.v;
• FOL/binFST_undec.v;
• FOL/Semantics/FiniteTarski/DoubleNegation.v;
• FOL/Utils/FriedmanTranslation.v;
• FOL/Utils/FriedmanTranslationFragment.v;
• FOL/Reductions/H10UPC_to_FOL_friedman.v;
• FOL/Reductions/H10p_to_FA.v;
• FOL/Reductions/binZF_to_binFST.v;
• FOL/Reductions/ZF_to_FST.v;
• SOL/Util/PA2_facts.v;
• TM/Reductions/SBTM_HALT_to_HaltTM_1.v;
• TM/Reductions/HaltTM_1_to_SBTM_HALT.v.

[DmxLarchey]

@mrhaandi considering that I did not contribute to the remaining files, I am going to push the PR in this state, letting the -notation-overridden option active in _CoqProject.

Then, I will file a new PR and associate @dominik-kirst to that so he can check that I am not proposing unwanted changes in that code, or possibly contribute updates himself.

[mrhaandi]

Shortly, I'll have a change to your PR which will address TM and SOL.

[mrhaandi]

See DmxLarchey#15 for TM and SOL.

[DmxLarchey]

See DmxLarchey#15 for TM and SOL.

For the record, I tried to inspect your PR but it fails and I do not understand why. It does not seem permission related.

larcheypc theories % gh pr checkout mrhaandi:notation-overridden
Depuis github.com:DmxLarchey/coq-library-undecidability
 * branch              refs/pull/15/head -> FETCH_HEAD
fatal: Pas possible d'avancer rapidement, abandon.
failed to run git: exit status 128

[mrhaandi]

For the record, I tried to inspect your PR but it fails and I do not understand why. It does not seem permission related.

Possibly because your PR is further in the history and one needs to rebase or merge my PR to avoid conflicts.

[DmxLarchey]

Well the issue was not (commit) history related. I have not found out the explanation.