coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FMapFacts functor

From: Aaron Bohannon <bohannon AT cis.upenn.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] FMapFacts functor
Date: Tue, 19 Oct 2010 14:58:05 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=vvcu59de5G+Qm+W7KUHbYvCVaZ3VcEYL8/uzuYI5d8J/iVmi0oILTxrYZSv/E3+8KL bYtXMtGUHiQXULDxS1wXAaBNXuN5Otl2Ye71NqcfrimQbnN+aqoQRHp2sxyr+MY9pFoX 39znfiEKA1rssJmzSUSEbW9vhONlPJsrHr6GY=

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.

Am I mistaken?  (Fortunately, this functor definition can easily be
inlined if necessary...)

- Aaron

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