Ssreflect Users Discussion List

[Guillaume Melquiond <>]

Le jeudi 14 octobre 2010 à 10:47 +0200, Edsko de Vries a écrit :

> [edsko@devriese2 ~/csw/src/ssreflect-1.2/src]
> # coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
> File "/var/folders/kg/kgA4gpp3Gnu+Kv5tWCp9yE+++TI/-Tmp-/coqmaindd09f5.ml",
> line 2, characters 17-29:
> Error: Unbound module Coqide
> 
> I'm not sure what exactly the error means and how I could try to fix
> it.. Any suggestions?

There was a similar discussion on this very list yesterday. Your symptom
is a bit different so it may be a different issue, but I'm still copying
it here in case it helps:

"At a time, Coq was not properly installing its interface files. In
particular, the /usr/lib/coq/ide directory was more or less empty. It
should at least contain coqide.cmi, coqide.cmx, ide.a, ide.cma,
ide.cmxa. (Your error is caused by coqide.cmi missing.)"

Best regards,

Guillaume