The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

> Hi, thanks for the report. I'll try to solve this issue by making
> these hints local to the FSets modules, and export them only in
> seperate, optional modules. I'll let you know when this is done.
> I'll also check with Elie Soubiran and Matthieu Sozeau whether
> we adequately avoid now registering several instances for the
> same constant if it has several names for the module system.

I am not sure this will be sufficient :
inside the module M, we do want FMaps/FSets hints. Therefore, we will
have to instantiate these separate optional modules at some point
(internally). From this point, it seems to me that there is no way to
prevent the hints from flowing away.

I might be wrong, but I really think the problem is not (only) with
the FMaps/FSets library, but with the hints declaration mechanism.

Namely, if I "Import N" in a module P, I certainly want hints of N to
be available in P, but not necessarily in modules that import P (N
might be a private module).
on the contrary, if I "Export N" in P, hints of N should certainly be
available to modules that import P (as it is currently the case).
I don't know what should happen when N is just "Required"...

Damien