The Coq mailing list

["Robert" <robdockins AT fastmail.fm>]

I'm trying to migrate a small proof I've done to use modules because I
think 
it will make things easier in the long run.   However, I'm running into
a 
problem that I don't know how to solve.  Coq is complaining when I try
to 
form certain kinds of modules, claiming
   "Signature components for label ... do not match"

I've attached a short proof script that demonstrates the problem for me.
 Is 
this a bug or is there some subtlety of module type-checking that I have 
missed?

coqcop reports
  "Welcome to Coq 8.1 (Feb. 2007)"


Many Thanks
Rob Dockins
-- 
  Robert
  
robdockins AT fastmail.fm

Attachment: ModProb.v
Description: Binary data