*response* window is too small when proof-shrink-windows-tofit is t
The issue reveals itself only after resizing emacs window (or zooming in/out with zoom-frm package – zoom-frm-in/zoom-frm-out commands):

I'm not completely sure about the steps for reproducing this issue, maybe my other settings affect this somehow.
GNU Emacs 27.0.50 (build 1, x86_64-apple-darwin18.2.0, NS appkit-1671.10 Version 10.14.1 (Build 18B75)) of 2018-11-08
My coq emacs config: https://gist.github.com/vyorkin/0675eefd5c572b3b0c0c76cf91a7ddd4
I also happens to me sometimes but I could not yet understand in which conditions this happens. It may be due to the use of symbols, which may make lines thicker than the font says. It could make the computation of the window height wrong. Next time this happens can you try to disable symbols and see if this solves the problem please?
sure, will do, thanks for the advice