Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: Thomas Refis <thomas.refis AT gmail.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin
  • Date: Tue, 23 Jul 2013 14:13:20 -0700

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 .




Archive powered by MHonArc 2.6.18.

Top of Page