coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: t x <txrev319 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Set Printing Implicit => "Use CoqIDE display menu instead"
Date: Thu, 18 Jul 2013 16:07:41 -0700

Hi,

I'm wondering if there's a solution to this (besides "use proof general" :-) )

I'm using Coq inside of Vim, which is running coq via "coqtop.opt -ideslave"

In trying to debug one of my tactics, I want to execute:

"Set Printing Implicit."

Unfortunately, I get back the response

"Use CoqIDE display menu instead."

Thus, I'm wondering:

1) Does the CoqIDE display menu send a different message to "coqtop.opt -ideslave"?

2) And if so, how can I mimic this message?

Thanks!

[Coq-Club] Set Printing Implicit => "Use CoqIDE display menu instead", t x, 07/19/2013
- Re: [Coq-Club] Set Printing Implicit => "Use CoqIDE display menu instead", Pierre Boutillier, 07/22/2013