coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Compilation error in coqide (8.1)

From: Ralph Matthes <matthes AT irit.fr>
To: Edsko de Vries <devriese AT cs.tcd.ie>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Compilation error in coqide (8.1)
Date: Thu, 08 Mar 2007 18:40:44 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Edsko de Vries wrote:

Hi,

When I try to compile coq 8.1 with the IDE enabled, I get the following
compilation error:

OCAMLC    ide/undo.ml
The implementation ide/undo.ml does not match the interface ide/undo.cmi:
Class declarations do not match:
class undoable_view :
   ([> Gtk.text_view ] as 'a) Gtk.obj ->
   object

Hello,

This reminds me heavily of the Coq bug No. 1216 I had submitted on September 12, 2006. Please see my conclusions on http://pauillac.inria.fr/bin/coq-bugs/not%20a%20coq%20bug?id=1216;user=guest
why I did not consider it a bug in the end.

I hope this helps.

Cheers, Ralph

*

*

[Coq-Club]Compilation error in coqide (8.1), Edsko de Vries
- Re: [Coq-Club]Compilation error in coqide (8.1), Ralph Matthes
- Message not available
  - Re: [Coq-Club]Compilation error in coqide (8.1), Edsko de Vries
    - Re: [Coq-Club]Compilation error in coqide (8.1), Samuel Mimram