Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] idtac and other msgs in PG

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] idtac and other msgs in PG


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] idtac and other msgs in PG
  • Date: Mon, 15 Dec 2014 11:04:49 -0500

On 12/15/2014 10:13 AM, Pierre Courtieu wrote:
Hi Jonathan,

Indeed pg is a bit out of sync with coq trunk currently.

I am trying to save some time to fix it. I aim at maintaining the same kind
of features as for coq 8.4. Understand: I don't have enough time to
implement something using asynchronous protocol for now. Maybe later if
other emerging interfaces do not grow mature enough.

Best regards,
Pierre

Thanks, Pierre! Not having the asynchronous protocol is not a problem for me (it doesn't work well with my scripts in CoqIDE due to my use of extraction after most function definitions).

-- Jonathan



Le Sat Dec 13 2014 at 5:27:27 PM, Jonathan
<jonikelee AT gmail.com>
a écrit :

For a while now I've been flipping back and forth between using PG and
CoqIDE, mostly because for some reason PG no longer shows idtac messages
(and other non-failure messages, such as from the Time command) in most
cases. It only shows them when the message-producing tactic also solves
the goal.

I'm wondering if anyone else has this issue with idtac in PG, or if I
somehow have it misconfigured.

I'm using a recent trunk version of Coq and the most recent development
version of PG (which is more than a year old).

-- Jonathan






Archive powered by MHonArc 2.6.18.

Top of Page