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
