The Coq mailing list

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