The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

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!