The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Hi Coq-users,

I installed coq8.4beta and found some weird behavior of the new "bullet" 
tactic.

Whenever I execute the bullet "-" followed by some tactic c, the proof
general displays the goal before executing the tactic c even though c
was indeed executed.
I looked into what "coqtop -emacs" does and found that it actually
prints out two consecutive goals: one before executing c and one after
executing c.
What I want to see in proof-general is the latter, but what it shows
me is the former.

Is this a bug in Coq, or a bug or my misconfiguration in ProofGeneral 4.1?

Best,
Gil

Here is a simple example.
--------------------------------------------------------------------
coqtop -emacs

<prompt>Coq < 1 || 0 < </prompt>Goal forall n, n = 0.
1 subgoal (ID 3)

  ============================
   forall n : nat, n = 0

(dependent evars:)

<prompt>Unnamed_thm < 2 |Unnamed_thm| 1 < </prompt>- destruct n.
1 subgoal (ID 3)

  ============================
   forall n : nat, n = 0

(dependent evars:)

<prompt>Unnamed_thm < 3 |Unnamed_thm| 2 < </prompt>2 subgoals, subgoal 1 (ID 
7)

  ============================
   0 = 0

subgoal 2 (ID 9) is:
 S n = 0

(dependent evars:)

<prompt>Unnamed_thm < 4 |Unnamed_thm| 3 < </prompt>
-------------------------------------------------------------------------