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 <[email protected]>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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
