The Coq mailing list

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

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

Require Import LongModuleName

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.

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