The Coq mailing list

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

I am a Coq novice.  I am looking for a way to

Require LongModuleName as LMN

so that instead of referring to a term foo in LongModuleName as
LongModuleName.foo, I can refer to it as LMN.foo.  I think the Agda
equivalent is

import LongModuleName as LMN

How do I do this in Coq?

Thanks and cheers,
Raghu.

PS: My apologies if you receive multiple copies of this message.  I
posted this through Gmane a few hours ago, but it hasn't appeared in the
list archives, so I am reposting it.

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