The Coq mailing list

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

Dear Raghu,

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.

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: Sunday, August 09, 2015 10:08 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Qualified imports

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/

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