Time Command + bullets = PG hangs

[jonleivent]

When Coq->Settings->Time Commands is set, and one issues Process whole buffer on a buffer with just the following:

Require Import Omega.

Goal forall n, n >= 0.
Proof.
induction n.

• omega.
• omega.
  Qed.

Then PG will hang just prior to the first bullet.

[Matafou]

Hi, thanks for reporting.

This looks like a coq bug to me. in coqtop, when typing "-" this is considered as a command (the goal and the prompt are printed). Whereas "Time -" seems to be considered as an incomplete command.

P.

[Matafou]

I submitted a bug report to coq. Meanwhile I will try to fix this by not putting "Time" in front of bullets.