"use" in drivers is done too late
After the merge of ComputerEuclideanDivision, we have errors for Alt-Ergo 2.0.0:
goal ..., prover 'Alt-Ergo 2.0.0': internal failure ' Ident infix > is not yet declared'
These happen when Alt-Ergo is called after inline_all, which eliminates the declaration of ">".
This particular problem can be fixed by rewriting the imported module avoiding ">" (which is ugly but will work), but the general issue is that anything imported via the driver does not go through the same transformation chain as the rest of the task.
I do not see a good solution for this right away. In fact, "use" in drivers starts to see inherently risky for me. Maybe we should simply rethink the treatment of EuclDiv and CompDiv for each major prover, aiming to have a good and sound translation in each case?