The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le mercredi 17 octobre 2007 à 06:42 -0400, Benjamin Pierce a écrit :
> Hi,
> 
> I have a module that defines several names, and I would like to make  
> just a subset of them available as unqualified identifiers in some  
> other scope.

> Is there a better way to achieve the effect I'm after?

Not sure it is a better way, but this is how I solved a similar issue:

        Module A.
          Module A_private.
            Definition a := O.
          End A_private.
          Import A_private.
          Definition b := a + O.
        End A.
        Import A.

Only "b" is directly usable here, "a" is not ("A_private.a" is), yet "a"
is directly usable inside "A".

Best regards,

Guillaume