| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Should replace C-c C-v at some point. Needs to have a complete list of
such queries. Obeys C-u prefix for Printing all flag.
|
|
|
|
Was making scripting confused.
P.
|
|
|
|
If enabled, allows to send queries to coq with
(control/shift/control-shift) mouse-1.
|
|
This comes from Hendrik's compile mode and is actually needed even
when this mode is off. When switching scripting buffer, restart the
coq shell process, so that it applies local coqtop options.
|
|
So that shortcuts work from this buffer.
+ colorizing.
|
|
|
|
After some command detecting things at point, the indentation was broken.
|
|
the emacs bug seems solved: the error with read-only always occur
whatever locale is used. So I toggle read-only off in
coq-compile-response.
|
|
|
|
No shortcut yet but I am testing some "one click" stuff right now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Added an option about that in proof-config.
To check: I adapted proof-treee regrexp accordingly.
|
|
|
|
It is the only way I found to display informativemessage appearing
*before* the goal.
|
|
|
|
|
|
|
