The Coq mailing list

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

The solution to my problem was very easy.
The functor MSetAVL.Ops takes not one but two argoments (I should have
checked more carefully).
The first argument is an implementation of the interface Int which is
used internally to measure the height of the AVL trees.
Thus the correct way to apply the functor is the following:

Module SSet <: MSetInterface.Ops StringLex := MSetAVL.Ops Int.Z_as_Int
StringLex.

Thanks anyway,
Marco

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