How do I import modules in Coq?

Question

I'm having trouble importing definitions from modules in Coq. I'm new to Coq, but couldn't solve the problem using the language's reference manual or online tutorial. I have a module that defines a signature and axioms for finite sets, which I intend to implement in another module. There's more to it, but it looks something like this (for reference, I'm closely following Filliatre's paper on finite automata):

Module FinSet.    
...
Parameter fset     : Set -> Set.
Parameter member   : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union    : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
  forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union    :
  forall A : Set, forall a b : fset A, forall x : A, i
    member x (union a b) <-> (member x a) \/ (member x b).
...
End FinSet.

I compile the module using coqc and attempt to load it into another module, say FinSetList or FinSetRBT, with the command Require Import FinSet. When I attempt to import the module, Coq (via Proof General) issues the warning:

Warning: trying to mask the absolute name "FinSet"!

Furthermore, I can't see anything defined in FinSet. How do I import the definitions (in this case, axioms) from one module into another? I essentially followed the steps outlined in Pierce's "Software Foundations" lectures. However, they aren't working for me.

Answer 1

Try adding to your .emacs file some explicit include paths:

 '(coq-prog-args (quote ("-I" "/home/tommd/path/to/some/stuff/lib" "-I" "/home/tommd/path/to/more/stuff/common")))