The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 12/16/2014 10:03 AM, Jonathan wrote:
> On 12/16/2014 08:27 AM, Pierre Courtieu wrote:
> > Hi,
> > with coq trunk version this should be better now. With proofgeneral cvs
> > (see below) version of today this should be even better.
> >
> > Best regards,
> > Pierre
>
> Thanks, Pierre!

One issue with the output is that now it is producing extra blank 
lines.  For example, I tend to use the following tactic to debug complex 
tactics:

Ltac vgoal :=
  idtac;
  match reverse goal with
    | H : ?T |- _ =>
      first[let v := eval cbv delta [H] in H in
            idtac H ":=" v ":" T
           |idtac H ":" T];
      fail
    | |- ?G =>
      idtac "======"; idtac G; idtac ""
  end.

This is now skipping 2 blank lines in PG between every non-empty idtac, 
and 1 black line in CoqIDE, so that I get output (in PG) that looks like:

Q : Prop


H0 : Prop


H1 : Prop


H : (H0 -> H1 -> Q)


======


H0


which makes using vgoal with goals that have many hypotheses cumbersome.

But, the perfect is the frenemy of the good, or at least they are not 
always BFFs ;)

-- Jonathan