The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

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

I'm doing things like:

    Module Export patch_sequences.
    Load unnamed_patch_sequences.
    (* Lots of coq *)
    End patch_sequences.

and if I load patch_sequences.v in coqide and "Go to end" then I get
this error:

    The term "up1" has type "UnnamedPatch" while it is expected to have
    type "patch_sequences.patch_sequences.unnamed_patches.UnnamedPatch".

i.e. I've ended up with 2 distinct UnnamedPatch types. I've tried some
other ways of importing, but haven't managed to find anything that
works.

A tar of my coq modules is here:

    http://urchin.earth.li/~ian/moduleproblem/moduleproblem.tar.gz

Can anyone tell me the right way to make and import modules, please?


Thanks
Ian