The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Apr 17, 2009, at 12:22 PM, Ian Lynagh wrote:

> I'm having trouble with coq's module system, and I can't work out what
> the right solution is.

Right now, your files seem to take the following form: For a file  
named foo.v, you have

        Module Export foo.
        Load bar.
        Load baz.
        (* Lots of Coq. *)
        End foo.

I believe the more idiomatic form of what you want is to have the  
following in foo.v:

        Require Import bar.  (* or Require Export bar. *)
        Require Import baz.  (* or Require Export baz. *)
        (* Lots of Coq. *)

This is the natural way (in my opinion) of treating foo.v as one  
compilation unit / one library file.  [Require Import bar] has the  
effect of making the definitions in bar available in the remainder of  
the current file, and you can refer to those definitions without the  
need for qualified names.  (This does require, however, that bar has  
been compiled to a .vo file using coqc.)  This is how Coq's standard  
library is implemented, and it might be a good source of examples.

I believe [Load] works as if it takes the named file and cuts-and- 
pastes its contents into the current file at the specified location.   
This probably explains why you're getting multiple definitions of the  
same thing.

[Module foo ... End foo] concerns Coq's module system.  I tend to  
think of this as something separate from treating a file as a library.

I hope that helps,
Brian