The Coq mailing list

[Andrew McCreight <continuation AT gmail.com>]

The latest released version of CompCert is for Coq 8.1.  You will likely encounter many (minor) errors trying to get it to work with a more recent version of Coq, going by my experience with porting large code bases to 8.2.

On Mon, Feb 9, 2009 at 4:32 AM, 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