The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi,

I am trying to compile ssreflect. I have Coq installed through macports. At 
first I tried to install ssreflect with 8.2pl1 but that didn't work, as ocaml 
had since been upgraded to 3.12.0, which is not compatible with 8.2pl1. 
Although version 8.2pl2 is not yet available in macports, I modified the 
portfile to refer to 8.2pl2 (and disabled one patch which seems to have 
already been included in 8.2pl2) to upgrade Coq -- that seemed to go fine. 
Compilation of ssrcoq, following the instructions, then also worked fine 
(that is, compilation didn't give any errors). 

However, when I try to generate a version of coqide, things break:

[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?

-E