Pierre Courtieu
Pierre Courtieu
Indeed I didn't realize your nice completion mechanism was already using yasnippet. Can you explain how it interacts with regular yasnippet minor mode? It seems to live separately (which is...
Indeed PG support for isabelle has been discontinued for some years now. We are in eht process of focusing next version of PG on Coq only. We will need to...
Thanks, please proceed! That said the adaptability of PG to new provers is not our priority currently. We rather would like to adapt PG to modern asynchronous interaction protocols first....
Well spotted. Will try to fix this during summer.
It is our fault for sure, but it also comes from coq slowly changing its behaviour. I think it spontaneously prints the goal less often. We definitely need to refactor...
@hendriktews is it really a problem of adding to the action list? It looks to me that we need a way to issue a "Goal" precisely when there is *nothing...
Hi, thanks for reporting. Indeed the coq process reports an error and PG do not detect it. Strange.
Hi, I cannot reproduce with my 26.1. Can you give the complete content of your *Messages* buffer please?
I cannot see anything that would explain what you are experiencing. I don't think the warning abot pc-select can be the problem but it is worth a try. @cpitclaudel I...
This is a matter of taste imho. I can try to propose a customization variable for this. No guarantee since the indentation code is rather fragile.