Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "coqmktop -top" fail with unbound module error

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "coqmktop -top" fail with unbound module error


Chronological Thread 
  • From: Stéphane Glondu <steph AT glondu.net>
  • To: Beta Ziliani <beta AT mpi-sws.org>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] "coqmktop -top" fail with unbound module error
  • Date: Wed, 25 Jul 2012 14:26:12 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page