The Coq mailing list

[Jaap Boender <jaapb AT kerguelen.org>]

On Thursday 17 April 2014 18:57:35 Cedric Auger wrote:
> I guess that by "Resource" in your mail you meant "thing" (or the reverse,
> the point being that they identify the same thing), that in the example you
> have in mind, the constructors of thing really need S, and that you meant
> FSet (or MSet) and not WSet (which I have never heard of).

WSet is one of the modules defined by MSet. Anyhow, yes, thing and resource 
are the same thing, and your solution does work. I'd have sworn I'd already 
tried something similar, but obviously there was some error somewhere. Thanks!

  Jaap