The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Fri, Apr 17, 2009 at 04:04:08PM -0400, Brian Aydemir wrote:
> 
> 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. *)

Thanks, I have something working now.

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

Yes, that's why I was using Load; I assumed that it was the same as
Require Import, except loading from the .v rather than .vo.

I am worried I will get confused by out-of-date dependencies now; I
would be much happier if coqide had a run-coqc-if-out-of-date option.

> [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'm using Module rather than Section as coq wouldn't let me put

    Module DecidableName.
    Definition t := Name.
    Definition eq := @eq Name.
    Definition eq_refl := @refl_equal Name.
    Definition eq_sym := @sym_eq Name.
    Definition eq_trans := @trans_eq Name.
    Definition eq_dec := eq_Name_dec.
    End DecidableName.

    Module NameSet := Make(DecidableName).

inside a Section. And if I use neither Module nor Section then everyone
in #coq tells me off  :-)


Thanks
Ian