The Coq mailing list

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

At 2015-08-12T07:26:27Z, Soegtrop, Michael wrote:

> 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.

Thanks, I'd be interested to know how to hide the original name of the
module.

Cheers,
Raghu.

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