The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

Marco Maggesi 
<maggesi AT math.unifi.it>
 writes:
> First question.  It seems that the standard library doesn't provide
> yet an order on strings.  So I defined myself an OrderedType for the
> strings (see the attached file).  But, despite the fact that the Coq
> assures that my module satisfies the necessary signature, when I apply
> the functor MSets.MSetAVL.Ops I get the following error that I cannot
> track (this arrives at the very end of the attached file)
>
> Error: Signature components for label t do not match: types differ.

My first guess is that t isn't being marked appropriately transparent,
so coq isn't allowing them to be indentified.

  Tom