Pierre Courtieu
Pierre Courtieu
Sorry I didn’t get your point. What do you think org-mode has to do with?
Hi @fblanqui. This is a known bug of both company-coq (with `prettify-symbol` enabled) and pg (`unicode-tokens`). I am afraid we can't fix this until PG is based on a good...
I do agree with your opinion about pg keybindings but actually almost all short keystroke are already bound globally. It is considered bad practice for a major mode to override...
Yes it is exactly the problem. there is one way to fix this: to make coqtop -emacs always do "Show" just before printing an error. This was the previous behaviour...
Le mer. 11 sept. 2019 à 11:13, hendriktews a écrit : > Pierre, you are extending the action list in the middle of the process > filter. Because of the...
Next week should be ok for me. I am in Paris (GMT +1).
March 10 21:00 CET. msteams or any browser-compatible is OK for me.
Do you have particular subjects in mind for this telco? I would like to hear your opinion on coq's xml protocol(s): mature enough? Should we give them a(nother) try? etc.
I'll be there. I would like to understand better how we can get rid of this "goal not showing" bugs. It must not be too difficult but PG architecture makes...