The Coq mailing list

[Robert R Schneck-McConnell <schneck AT math.berkeley.edu>]

On Wed, 6 Oct 2004, Bruno Barras wrote:
> Adam Chlipala wrote :
> > I would like to check that a .vo file satisfies a certain "signature,"
> > in an ML-like sense.
>
> 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.

This works, to an extent, but it allows that A only *declares* the
required entities, as Parameters or Axioms.

Is there a canonical way to check or require that a module *defines*
all of its elements?

Robert