From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 2DF5BBC6C for ; Wed, 12 Dec 2007 22:57:15 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAHToX0fBAkMt/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.24,158,1196636400"; d="scan'208";a="5153801" Received: from vega.fmf.uni-lj.si (HELO postar.fmf.uni-lj.si) ([193.2.67.45]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Dec 2007 22:57:14 +0100 Received: from localhost (unknown [192.168.5.1]) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 7BC56239D00; Wed, 12 Dec 2007 22:57:13 +0100 (CET) X-Virus-Scanned: amavisd-new at spam.fmf.uni-lj.si Received: from postar.fmf.uni-lj.si ([192.168.5.5]) by localhost (spam.fmf.uni-lj.si [192.168.5.1]) (amavisd-new, port 10024) with ESMTP id Wussb-0lQ0lH; Wed, 12 Dec 2007 22:57:13 +0100 (CET) Received: from [192.168.1.107] (BSN-77-148-136.static.dsl.siol.net [193.77.148.136]) (Authenticated sender: bauer) by postar.fmf.uni-lj.si (Postfix) with ESMTP id 6834C239C97; Wed, 12 Dec 2007 22:57:12 +0100 (CET) Message-ID: <47605953.5000509@fmf.uni-lj.si> Date: Wed, 12 Dec 2007 22:57:39 +0100 From: Andrej Bauer Reply-To: Andrej.Bauer@andrej.com User-Agent: Thunderbird 1.5.0.14pre (X11/20071023) MIME-Version: 1.0 To: Arnaud Spiwack , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Coq 8.1 and Ocaml 3.10 References: <47601894.1080105@fmf.uni-lj.si> <47601B45.5090503@lix.polytechnique.fr> In-Reply-To: <47601B45.5090503@lix.polytechnique.fr> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; andrej:01 andrej:01 coq:01 ocaml:01 bug:01 camlp:01 bug:01 ocaml:01 coq:01 lattices:01 makefile:01 wrote:01 arnaud:01 caml-list:01 surprising:01 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". Andrej