Use From systematically

[proux01]

Motivation for this change

This is just adding From to every Require that did not already had one.

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Until now, when inside theories, we were using From mathcomp when referring to classical files and no prefix when referring to files from theories (same reasoning for other directories). I think it was necessary to make the CI goes through and, of course, as a developer, I got used to it as a piece of information when reading headers. Your PR shows that we can put prefixes everywhere and the CI still goes through, that looks more homogeneous butiIs there an advantage in having From prefixes everywhere? (I think that I am asking because of my lack of experience with the -Q option.)

[proux01]

-Q is the same as -R except that it makes From mandatory.
The main advantage I see to the uniform use of From is to make PR creating subpackages suc as #1349 much easier, otherwise they request the addition of a lot of From everywhere, making their diff completely unreadable. A side advantage is that if Coq people add a file in the prelude/Stdlib with the same name as one of ours, this avoids the conflict.
The small drawback is that we loose the documentation that "no From" means "in theories". We could recover it by using From mathcomp.analysis instead of From mathcomp, but not sure it's a good idea and it will somewhat minimize the first advantage (when spliting sub packages).

[affeldt-aist]

I was a bit bothered by the fact that we lose the information about which package are in the current directory but since the developers always put them last this is really a small price to pay to get new opam packages.

[proux01]

If you prefer, we could use From mathcomp.analysis to keep that information?

[affeldt-aist]

If you prefer, we could use From mathcomp.analysis to keep that information?

The discipline of keeping the local packages last is enough I think.