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: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] idtac and other msgs in PG
  • Date: Tue, 16 Dec 2014 01:10:34 +0900

Hi Jonathan,

I solved a part of the issue by this code:

Require Import Coq.Strings.String.
Open Scope string.

Definition newline := String "010" "".
Definition line s := s ++ newline.

Definition show_pg s := String "254" s ++ String "255" "".

Goal False.
let s := eval vm_compute in (show_pg (line "foo" ++ line "bar")) in
idtac s.
Abort.

Regards,
Kazuhiko

2014-12-14 1:26 GMT+09:00 Jonathan
<jonikelee AT gmail.com>:
> 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