The Coq mailing list

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

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.