The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi list,

I can create a new coq toplevel with the usual coqmktop command without any issues. Now, when I add the "-top" option, compilation breaks with the following message:


$ ~/coq-8.4beta2/bin/coqmktop.byte -g -top  -o coqtop src/run.cmo src/runtac.cmo

File "/tmp/coqmain4bdbf3.ml", line 15, characters 57-67:
Error: Unbound module Util

I compiled coq with the options "-debug" and "-local".

Any suggestions on how to fix this?

Thanks in advance,
Beta