[NES] [wish] propagate extra logical stuff to enclosing module

[gares]

In NES @CohenCyril and I use modules (and the nametab) to simulate namespaces.
One thing seems impossible to achieve without modifying the Libobject system.

coq-elpi/apps/NES/examples/usage_NES.v

Lines 43 to 45 in 3eff594

	Fail Check @default _ : nat.
	(* This behavior requires Libobject to be aware of the role played by
	a module: if it is a namespace some "actions" have to be propagated upward *)

CC @maximedenes do you think this is feasible?

[Blaisorblade]

👍 this is one reason I abuse #[global], but it doesn't have quite the right semantics...

[Blaisorblade]

Oooh, seems that Export module(coercions, canonicals, hints) would fix this!
If NES generated that when closing a namespace, #[export] Instance inside a namespace would work well!

https://coq.inria.fr/refman/language/core/modules.html#coq:cmd.Import