When I begin stepping through a coq file the goal window opens to the right of the file window.
How does one configure emacs to display the goal window below the file window?
I tried using the transpose frames but it messes with proof general and other coq settings such as prettifying symbols.
Can I configure my
.emacs file to handle this?
You can definitely rearrange your windows once the scripting started. But you will probably need to do it again for each new file you script. So you should probably use a predefined display mode: vertical/horizontal/hybrid /smart. Citing doc(https://proofgeneral.github.io/doc/master/userman/Customizing-Proof-General/#Display-customization)
If you want to force one of the layouts, you can set variable ‘proof-three-window-mode-policy’ to 'vertical, 'horizontal or 'hybrid. The default value is 'smart which sets the automatic behaviour described above.
This can also be configured via the coq menu.
Thanks! I was able to find it in the coq menu!
Last updated: Feb 06 2023 at 07:03 UTC