Pierre Courtieu
Pierre Courtieu
Sorry to be unable to give a hint. Did you find the culprit?
We definitely need to do something like that. 1. find the time to implement the main loop (reuse the work done by psteckler?) 2. accept dependency with a plugin (serapi...
I just had a look at `elcoq.el` and it seems indeed quite simple and nice. I will give it a try when I have time, to better understand. In particular...
For the format of output for `Query` I don"t know. @cpitclaudel @erikmd do you have an opinion? How is the rendering of [html | xml | sexp]-ified terms and goals?...
> For example as I mentioned we should maybe make the calls take a position and not a statement id as to relieve emacs from synchronizing that stm_id table. I...
Thanks. This is a good idea. I will have a look at your patch asap. Can you explain how the user does specify the part of the goal to follow?...
Looks good and useful to me. Thanks again! @cipher1024 can you add a line to the CHANGES file, rebase into one commit please? We need to add a documentation on...
PG already shows the number of goals in the scripting buffer modeline. People hardly notice it I suppose. What exact display do you have in mind?
As you suggest we could show it in the goals buffer modeline of course. I suppose it is more intuitive.
Actually I have been thinking of enhancing further the coq/PG UI wrt to number of subgoals and also script parenthesizing ({ }) and bullets. Ideally I would like coq to...