The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Stéphane Lescuyer a écrit :
> 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.
>   
I am not so sure since Set is extracted to caml, but not Type (if I well 
understood).
If I replace Set with Type it may not extract it.
> 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
> >
> >     
>
>
>
>   


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay