The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 24/07/2012 15:46, Beta Ziliani a écrit :
> 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 <http://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?

This is a bug in coqmktop. Please file a bug report.

My guess is that your command works if you configure coq without -local.


Cheers,

-- 
Stéphane