The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

:) nice dirty trick.

I am currently adapting coq output so that emacs will notice messages more accurately. Should be working tomorrow.

Best regards.

P.C.

Le Mon Dec 15 2014 at 5:11:12 PM, Kazuhiko Sakaguchi <pi8027 AT gmail.com> a écrit :

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
>