coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FMapFacts functor

From: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
To: Aaron Bohannon <bohannon AT cis.upenn.edu>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] FMapFacts functor
Date: Fri, 22 Oct 2010 23:40:31 +0200

On Tue, Oct 19, 2010 at 02:58:05PM -0400, Aaron Bohannon wrote:
> The file FMapFacts contains the following line:
>
> Module WFacts (M:S) := WFacts_fun  M.E M.
>
> Is this a typo?  I think this is the intention:
>
> Module WFacts (M:WS) := WFacts_fun  M.E M.
>

Indeed. Thanks for noticing this one, it's now fixed in the trunk.

Best,
Pierre L.

[Coq-Club] FMapFacts functor, Aaron Bohannon
- Re: [Coq-Club] FMapFacts functor, Pierre Letouzey