I think I started learning Coq around March 2012, so it must have been
8.3pl3 or 8.3pl4.

Setting coq-end-goals-regexp-show-subgoals to nil does what I want (or, at
least, is plenty good).  Thanks for the workaround!

-Jason


On Fri, Apr 19, 2013 at 4:55 AM, Hendrik Tews <t...@os.inf.tu-dresden.de>wrote:

>
> I believe all Proof General versions (including the latest trunk)
> show the timing in the *goals* buffer when you use them with Coq
> 8.3pl4 or earlier. If you have more than one subgoal the timing
> is shown only when coq-hide-additional-subgoals is off. Then the
> *goals* buffer looks like
>
> ######################################################################
> 2 subgoals
>
>   ============================
>    True
>
> subgoal 2 is:
>  True
> Finished transaction in 0. secs (0.u,0.s)
> ######################################################################
>
>
> When coq-hide-additional-subgoals is on, only the text before
> "subgoal 2" is copied to the *goals* buffer, and then the timing
> is obviously only displayed when you have one subgoal.
>
> Coq 8.4 displays the dependent evar line under Proof General.
> Therefore, with Coq 8.4, Proof General only copies the material
> before the dependent evar line to the *goals* buffer, and the
> timing is lost.
>
> Jason, can you try setting coq-end-goals-regexp-show-subgoals to
> nil? (M-x customize-variable coq-end-goals-regexp-show-subgoals,
> Value Menu -> nil; State -> Save for furture sessions; then
> restart Proof General) Then the goals buffer looks like
>
> ######################################################################
> 2 subgoals, subgoal 1 (ID 3)
>
>   ============================
>    True
> subgoal 2 (ID 4) is:
>  True
> (dependent evars:)
>
> Finished transaction in 0. secs (0.u,0.s)
> ######################################################################
>
>
>
> Bye,
>
> Hendrik
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to