Skip to Content.
Sympa Menu

coq-club - [Coq-Club] problems while trying to recompile compcert with the trunk 11850

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problems while trying to recompile compcert with the trunk 11850


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page