Inlining in non-logical objects not granted in module definitions

[herbelin]

Description of the problem

Module Type EqType.
   Parameter Inline t : Type.
   Parameter eq : t -> t -> Prop.
   Notation "#" := t (only parsing).
End EqType.

Module NAT.
   Definition t := nat.
   Definition eq := @eq nat.
End NAT.

Module F (E:EqType) :=
  E.

Module Import NAT' := F NAT.
About NAT'.eq. (* no arguments scopes, because it is for the non-logical-objects purpose of type NAT'.t *)
About NAT.eq. (* arguments scopes have also been canceled *)
Check #. (* no inlining: NAT'.t *)

Contrastingly, it is ok with an Include:

Module F (E:EqType).
  Include E.
End F.

Module Import NAT' := F NAT.
About NAT'.eq. (* Arguments NAT'.eq (_ _)%nat_scope *)
About NAT.eq. (* Arguments NAT.eq (_ _)%nat_scope *)
Check #. (* nat *)

(explicit qualification with NAT' even when imported is from me, to emphasize the differences)

Fix possibly to come.

Coq Version

From 8.5 to master.