Disambiguate From ... Require Import|Export ...

Fix issue #49 (closed) by converting From rt.foo Require Import|Export bar. to Require Import|Export rt.foo.bar. all over the place.

This actually fixes a bunch of incorrect imports, i.e., we were accidentally relying on Coq's auto-magic search feature to find the intended modules.

Aside: We obviously have too many Require Import statements, but that will have to be addressed in a separate MR.

CC: @sbozhko @mlesourd @sophie @proux

changed milestone to %Prosa v0.4

This looks ok to me.

Regarding the verbosity of these statements I guess that strategic use of Require Export can improve the situation and we cannot do much better as long as the bug is present in coq.

Thanks for the feedback. The Require cleanup is pretty much done (see !68 (merged)); I'll merge this in one go once the rest of the cleanup is done. In the meantime, any comments on !68 (merged) would be appreciated.

merged