The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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?


Assume you want to check that A.vo has a signature compatible with a 
module type B.
You just have to do on the toplevel (or in a file):

Require A.
Module test <: B := A.

for instance:

Module Type S.
 Inductive nat:Set := O | S(n:nat).
End S.
Module test_ok <: S := Datatypes.
Require List.
Module test_not_ok <: S := List.

Hope this answers your question.

Bruno Barras.