coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] "coqmktop -top" fail with unbound module error, Beta Ziliani, 07/24/2012
- Re: [Coq-Club] "coqmktop -top" fail with unbound module error, Stéphane Glondu, 07/25/2012
- Re: [Coq-Club] "coqmktop -top" fail with unbound module error, Beta Ziliani, 07/25/2012
- Re: [Coq-Club] "coqmktop -top" fail with unbound module error, Stéphane Glondu, 07/25/2012
Archive powered by MHonArc 2.6.18.