The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2015-08-10T10:24:52Z, Soegtrop, Michael wrote:

> maybe there is a more elegant way, but what I did sometimes in such
> cases is to wrap it into a module like this:
>
>       Module L.
>       Require List.
>       Include List.
>       End L.
>
>       Print L.hd.

Thanks for the suggestion.  Meanwhile, I found that

  Require LongModuleName.
  Module LMN := LongModuleName.
  Print LMN.foo.

also works.  Is there any reason to prefer the one over the other?

Cheers,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/