Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.5 is out!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.5 is out!


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq 8.5 is out!
  • Date: Mon, 25 Jan 2016 11:27:48 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
  • Ironport-phdr: 9a23:MqtKFB8lqyP5Bf9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdudsqscwLOM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU1p3vnLnos7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCaJ/HoXVS0qmwFTAkCR4RfgX5z29DfzrfF88CicJ8z/C74uD2fxp5x3QQPl3X9UfwUy93va35R9
On Mon, Jan 25, 2016 at 11:22:07AM +0100, Frédéric Blanqui wrote:
> Hello Enrico.
>
> I was just trying to use your new compilation procedure but I get errors.
> But I am not sure how to proceed. It's perhaps better to discuss this
> offline first.
>
> time make -j20 quick:
>
> Error: The value you are asking for (matching_complete) is not available in
> this process. If you really need this, pass the "-async-proofs off" option
> to
> CoqIDE to disable asynchronous script processing and don't pass "-quick" to
> coqc.

This must be the limitation affecting the "Include" directive of the
module system. See
https://coq.inria.fr/bugs/show_bug.cgi?id=4066

Best,
--
Enrico Tassi

Archive powered by MHonArc 2.6.18.

Top of Page