Pierre Courtieu
Pierre Courtieu
There is an overlap, but this list is very conservative (it is for passing command to coq directly via the minibuffer (`C-c C-v`).
Seems ok. We need to remove a nombre of commands from this list I think. I see a few that are state changing (Opaque etc). Don't even know why they...
That sounds like a good idea. That said the `STATECH` boolean has not been correctly maintained for a long time, and we don't rely much on it. This change would...
Hi there, wouldn't it be the time to consider submitting Coq in Hal in the "software" category? I don't know exactly since when this is possible, but it is there...
At the time this splash screen was created (before I ever used pg) emacs used to freeze for a few seconds while PG was initializing and the user was tempted...
Sure. Sooner is better imho.
I think this is standard in emacs. You define comment starters and enders in the syntax table. This is a bit convoluted for two-letters comment delimiters: Look at https://www.gnu.org/software/emacs/manual/html_node/elisp/Syntax-Descriptors.html You...
I think [this](https://stackoverflow.com/questions/15718599/single-and-multiline-comments-in-emacs-mode-using-syntax-table) should help.
It is used in the generic code of proofgeneral. In particular when PG splits a file into a sequence of commands and comments. Otherwise a comment is "glued" to the...
I think the gluing behaviour becomes optional when these variables are set. I don't know if this is documented but I just grepped "comment-start" in the generic directory and this...