coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <Cedric.Auger AT lri.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] problems while trying to recompile compcert with the trunk 11850
- Date: Mon, 09 Feb 2009 13:32:47 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] CALCULEMUS 2009 - Final Call for Reviewed Papers, Sean Wilson
- [Coq-Club] problems while trying to recompile compcert with the trunk 11850, Cedric Auger
Archive powered by MhonArc 2.6.16.