The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Cedric,

OrderedType.t and FSetInterface.S.t used to be of type Set. This
prevented (for no reason) developers to build finite sets whose
elements were in Type and not in Set. For that reason they have both
been changed to Type which is a very wishable update indeed, but leads
to some incompatibilities with earlier developments. It should be
fairly straightforward to fix your files, by changing the appropriate
occurrences of Set to Type.

Cheers,
Stéphane

On Mon, Feb 9, 2009 at 1:32 PM, Cedric Auger 
<Cedric.Auger AT lri.fr>
 wrote:
> Hello, I tried to recompile compcert using the trunk version 11850, and
> found:
>
> COQC lib/Lattice.v
> File "/users/demons/cauger/Documents/compcert-1.3/lib/Lattice.v",
> line 325, characters 0-10:
> Error: Signature components for label t do not match.
> make: *** [lib/Lattice.vo] Erreur 1
>
> I tried to understand what happened:
> it seems that in contrary to
> http://coq.inria.fr/library/Coq.FSets.FSetInterface.html ;,
> S.t is no longer of type Set but of type Type.
>
> I think, that there has been a non wishable correction in some update; am I
> wrong?
> Is it an old bug that has been corrected since?
>
> --
> Cédric AUGER
>
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06