coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Leveraging the module system

From: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
To: Taral <taralx AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Leveraging the module system
Date: Sat, 31 Jan 2009 16:56:09 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I had tried that. However, SIG is the Module Type of a Functor of one argument, so alone it is not a module type. I receive the error "User error: The result module type must be a signatue"

Scott Doerrie

Taral wrote:

On Fri, Jan 30, 2009 at 1:15 PM, M. Scott Doerrie
<mdoerri AT cs.jhu.edu>
wrote:

Module Impl (P:SIG2).

Module Impl (P:SIG2) : SIG.

[Coq-Club] Leveraging the module system, M. Scott Doerrie
- Re: [Coq-Club] Leveraging the module system, Taral
  - Re: [Coq-Club] Leveraging the module system, M. Scott Doerrie
- Re: [Coq-Club] Leveraging the module system, Elie Soubiran
  - Re: [Coq-Club] Leveraging the module system, M. Scott Doerrie
  - Re: [Coq-Club] Leveraging the module system, M. Scott Doerrie