[NES] export/include namespaces

[pi8027]

I wish a feature to export/include a namespace from/in another namespace. Unlike the Export command, exporting A from B should probably make A.blabla accessible as B.blabla. So its behavior is perhaps closer to Include.

I think this is one of the missing features (besides #181) for replacing the use of modules with NES in MathComp, especially in ssralg.v, where lemmas are first proved in GRing and then copied in GRing.Theory (to make them available as both GRing.blabla and GRing.Theory.blabla, of which users may import only the latter because the former contains the stuff that should not be accessible with shorter names, e.g., GRing.add). IMO, this behavior should be achieved by proving them in the GRing.Theory namespace and exporting them from GRing.

[CohenCyril]

I cannot recall a reason why they cannot just be in the GRing.Theory namespace (which can be open anywhere). Do you?

[pi8027]

IIUC, the reason is that this duplication allows users to access these lemmas with qualified names GRing.blabla (not GRing.Theory.blabla) even if they don't import GRing.Theory. But, I have the impression that almost no one is (intentionally) using this feature.

[pi8027]

Related issue on the MC side: math-comp/math-comp#1303