English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Coq 8.1 and Ocaml 3.10
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-12-12 (21:57)
From: Andrej Bauer <Andrej.Bauer@f...>
Subject: Re: [Caml-list] Coq 8.1 and Ocaml 3.10
Arnaud Spiwack wrote:
> This bug seems to have nothing to do with camlp4/5. I've seen this bug
> twice before, with two different version of OCaml (3.09.3 and 3.09.2
> namely), but always Coq 8.1pl2. It's rare, and I have no clue why they
> occur.

I don't insist, I just want a Coq which doesn't think that semirings
satisfy the cancelation law for addition (since I care about
distributive lattices, which are semirings without a cancelation law).

> One solution is to move to the trunk version of Coq (whose Makefile has
> been reengineered, and is far less surprising).

Will try an older version of Coq first. Thanks for the advice. I just
wanted to hear from someone that Coq was "Ocaml 3.10 ready".