A simple extension for PG which detects when the current subgoal, annotated with a bullet, is proved (after C-c C-n command) and automatically inserts a proper bullet for a next sibling subgoal or for a sibling of the goal (if last subgoal is proved).
Nice idea. Does it always insert a bullet or does it try to be smart by looking if it is already there?
My question is more: what is the heuristic to trigger the insertion ?
PG has an Emacs hook for processing content of last response from coqtop where a regex match is the trigger. C-c C-n interceptor in form of elisp function advice makes sure that hook is working once after an evaluation step.
My question is from a user experience perspective: surely when I script my already written script line by line I don’t want new bullets to appear and make everything wrong. Sot he question is: when is the bullet actually inserted in the buffer?
The bullet is inserted only if it is missing.
Hi! thanks for implementing this nice feature!
Other question: what are the Coq versions supported?
(I guess it depends on the first version of Coq that outputs “…Focus next goal with bullet…” ?)