The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

2 days ago I answered :

Le 19 juil. 2013 à 01:07, t x <txrev319 AT gmail.com> a écrit :

> 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"?
it sends <call id="-2" val="interp" raw="">Set Printing Implicit.</call>
>  2) And if so, how can I mimic this message?
you should add the 'raw=""' in your call :-)
> Thanks!
Cheers,
Pierre B.

Le 23 juil. 2013 à 23:13, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

Thanks for that example.

When I send "Set Printing Universes."  or other set command , (coqtop -ideslave) replies back :

<?xml version="1.0"?>

<value val="fail" loc_s="0" loc_e="23">

Error: Use CoqIDE display menu instead</value>

How do I get around this?

Thanks

On Tue, Jul 23, 2013 at 2:17 AM, Thomas Refis <thomas.refis AT gmail.com> wrote:

2013/7/23 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

> I think I know that I'm doing something wrong. when I process the line +
> Case "->";  auto.  ,
> I need to send it to CoqTop in 2 steps. First send "+ " and then "Case "->";
> auto."

Precisely.
Note that you get the same behavior when you send something after a
dot (i.e. it is ignored), see http://paste.awesom.eu/IFp .