The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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 .