The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 06 oct 2004, Adam Chlipala wrote:

> I would like to check that a .vo file satisfies a certain "signature," 
> in an ML-like sense.  I want to create a file with a list of identifiers 
> and their types, possibly with earlier identifiers bound in the types of 
> later identifiers.  Then, I want an automated tool to check that a 
> certain .vo file defines each identifier with a type equivalent to the 
> one I have specified.  It would also be fine to be able to perform a 
> series of actions in coqtop and then ask it to check that identifiers 
> have been defined according to a given signature.  Is there a canonical 
> way to do this with Coq?
> 
> Thanks!

I think you are on road to use modules! Signatures are exactly what module 
types are made for. See the manual for explanations and examples. You can 
also read the Coq'art book of Yves Bertot and Pierre Casteran, where the 
module system is explained in great detail.

Pierre