The Coq mailing list

[Tom Hutchinson <thomas.hutchinson AT sophia.inria.fr>]

Was your lablgtk2 installed with an rpm (or manually by source)?

If it's an rpm, then maybe you need to install lablgtk2-devel. (I don't know 
much about OpenSUSE so it's just a guess)

I compiled CoqIDE with lablgtk2 2.14.0. Still, the file /ide/utils/okey.ml 
hasn't been changed in years. I would be surprised if it required a really 
recent lablgtk version.

http://docs.camlcity.org/docs/godipkg/3.10/godi-lablgtk2/lib/ocaml/pkg-lib/lablgtk2/gdk.mli
It looks like there is a Gdk.Tags.modifier
This is from 2.12.0 (see bottom: 
http://docs.camlcity.org/docs/godipkg/3.10/godi-lablgtk2)

Tom

On Mar 26, 2010, at 12:04 AM, Jianzhou Zhao wrote:

> Hi,
> 
> I got the error when compiling 8.3:
> 
> ./ide/utils/okey.mli line 33
> Unbound type constructor Gdk.Tags.modifier
> 
> This seems a problem from Lablgtk2:
> http://caml.inria.fr/pub/ml-archives/ocaml-beginners/2004/01/c57a676198b126994795763abf5ad5b1.en.html
> 
> I used
>  Camlp5 version 5.13 (ocaml 3.11.0)
>  Lablgtk2 with 2.12.0
>  OpenSUSE 11.2
> What is the correct Lablgtk2 CoqIDE needs?
> 
> I remember I had the same problem when I compiled 8.2 last year,
> and commented CoqIDE compilations.
> 
> Thanks
> -- 
> Jianzhou