feat(coq): insert named goal selectors

[dhalilov]

This PR implements the coq-insert-named-goal-selectors function that automatically generates named goal selectors (of the form [name]: tac.) for each open named goal. I bound it to C-c C-a C-g by default.

The implementation is based on the output of Show Existentials, and notably checks for the absence of (only printing) in the output to distinguish focusable goal names from unfocusable goals (see rocq-prover/rocq#20809).

This feature is mainly intended to be used in conjunction with automatically named goals in Rocq 9.2.

Here's a demo:

[rswarbrick]

Hi there! I was feeling enthusiastic about reading some elisp again, so I thought I'd go through and leave a review. I hope it's useful!

[dhalilov]

Hi there! I was feeling enthusiastic about reading some elisp again, so I thought I'd go through and leave a review. I hope it's useful!

Hey @rswarbrick, thanks for the review! Agreeing with all of your comments, I'll make the appropriate changes promptly.

By the way, coq-insert-snippet-with-holes was extracted verbatim from the implementation of coq-insert-match to avoid code duplication, but I've just found out that holes.el provides holes-replace-string-by-holes-backward-jump which has exactly the same implementation, so I might use that instead :)

[rswarbrick]

This looks good to me. I did a re-review and realised that all the stuff that had made me raise my eyebrows is now deleted! :-D

[Matafou]

Hi! Very nice idea! I want to merge but I have one question first.

I see that you sneaked into holes.el (which I thought nobody cared about). But I am planning to remove holes.el in a short future and rely on yasnippet instead (opt in). What do you think of that? I will adapt your code when this happens of course.

[dhalilov]

I see that you sneaked into holes.el (which I thought nobody cared about). But I am planning to remove holes.el in a short future and rely on yasnippet instead (opt in). What do you think of that?

I used holes.el since that was the solution used in coq-insert-match, but I would definitely be in favor of using yasnippet 😄

[Matafou]

Thanks @dhalilov and @rswarbrick !