On 2016-08-04 22:17, Tej Chajed wrote:
>>> Perhaps using ‘buffer-list-update-hook’ instead of advising
>>> `select-window' would help?
>
> I haven't fully debugged this alternative, but it doesn't seem to
> work. company-coq still uses save-window-excursion in
> company-coq-ask-prover, which triggers the buffer-list-update-hook. 

IIRC I added this save-window-excursion call to work a Proof General issue, back when I didn't know much about PG.  Now that I have commit rights there, I could probably move the fix upstream and remove the save-window-excursion call.

Clément.