The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

You can certainly define Module Short := LongName.

On 8 September 2013 22:18, Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com> wrote:

I meant "Other" instead of "B" in the last Import.

2013/9/8 Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>

Hi CoqClub,

This is a beginner's question. Suppose you have two files:

LongName.v
   Inductive an_inductive_type :=
      a_constructor : an_inductive_type

Other.v
   Inductive an_inductive_type :=
      a_constructor : an_inductive_type

(same names!)

Combined.v
Require Import LongName
Require Import B

Inside the file Combined, the only way I know of indicate to Coq which one is the
constructor I want is by using LongName.a_constructor.  But I wonder if there is a better way, like giving a scope name as we do with Notations. Or giving a shorter alias to LongName.v. Not sure if the Module system (I never used it) could help me.

Thank you.