fix #596 - outdated documentation for setup coq-prog-xxx.

[Matafou]

Fix #596

I did a refresh on this part of the documentation.
I propose to merge this before adapting maybe according to #590.

[Matafou]

I will merg e this soon if noone objects.

[erikmd]

Thanks @Matafou; I did a quick review and left very minor suggestions

[erikmd]

Are you sure you want to remove this documentation from now on? 😉
but maybe you'd have plans to port part of the features of Holes to the same "elisp backend" as that of company-coq?

[Matafou]

Indeed. I made a small poll on Zulip and it appear I was the only user of this feature.
I have tested yasnippet snippets for coq and it works quite well and it does not interfere with company coc completions (even if it also uses yasnippet). There are a few editing tricks that I will miss but nevermind.

[Matafou]

More precisely I plan to

1. remove everything from the holes library shortly.
2. document and/or propose a set of user-customized abbreviations (unless this subsumed by company-coq maybe)
3. one day maybe try to reimplement the copy-paste-in-the-holes thing, even if nobody seems to be willing to try it...

[erikmd]

So feel free @Matafou to merge this when you see fit.

BTW, small remark: it happens there are 3 PR merging strategies in GitHub (Merge, Merge/Squash, Merge/Rebase),
and I believe you have recently used the Merge/Rebase one? (maybe)

It seems actually that Merge/Rebase has two drawbacks:

• there is no mention anywhere of the PR number in the resulting commits messages;
• and the resulting commits are not GPG-signed (cf. the missing Verified slug on those commits).

However, Merge and Merge/Squash are very fine − Merge/Squash being especially fine if the PR contains only one commit I guess.

So, maybe for merging upcoming PRs we should only use Merge or Merge/Squash 😅

(I guess I could copy this suggestion in the wiki later on? Cc @cpitclaudel @hendriktews @Matafou @monnier FYI)

[erikmd]

(I guess I could copy this suggestion in the wiki later on? Cc @cpitclaudel @hendriktews @Matafou @monnier FYI)

Done FYI: https://github.com/ProofGeneral/PG/wiki/Checklist-for-testing-and-reviewing-a-PR#merging-a-pr

[Matafou]

Thanks @erikmd.

[Matafou]

BTW @erikmd sorry for the rebase, this is the default "merge" button behaviour.

[erikmd]

No worries for this time ;)
Actually it's not the default action for me... so I believe the "default" action is just the last one used by the logged-in user. So to change it we need to use the drop-down list I guess.