The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Raghu,

the reason why I did it with the require inside of a module is that I thought 
that then the module would not be known under its original name. But just 
testing it, I found this is not the case (Print List.hd works). I am quite 
sure I somehow managed to do this in some way like this - I need to look into 
some old files in case you need this.

If you don't care if the module is also known under its original name, then 
the simple module assignment should be the better way.

Best regards,

Michael


-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of N. Raghavendra
Sent: Tuesday, August 11, 2015 8:37 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Qualified imports

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/

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928