The Coq mailing list

[Marco Maggesi <maggesi AT math.unifi.it>]

Thank you Tom for you suggestion.
In fact I also made several attempts at how the signatures are imposed
on my modules.
For instance, i tried to use "with" like in

Module StringLex <: (OrderedType with Definition t := string) :=
DSO_to_OT DSO_String.

No one of these tricks helped so far.

Marco


2013/1/3 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