Fix checkdoc warnings

[MorganJamesSmith]

Hello! I am new to contributing to ProofGeneral.

Emacs now has a builtin utility called checkdoc to check docstrings and general file format. It also enables running a spell checker on all the docstrings.

Here I have added a make target to run this utility along with a dictionary of words that I assume are not typo's yet are not found in my ispell dictionary.

Running checkdoc yields 779 warnings. I have gone through an fixed most of them and I am now down to 29 warnings.

Please let me know what you think. Thank you for taking a look!

[MorganJamesSmith]

I just rebased this and fixed all merge conflicts

[Matafou]

Hi @MorganJamesSmith and many thanks for this contributions. I will merge this soon (after re-basing it).

[MorganJamesSmith]

Thank you @Matafou . I used the commits you provided at MorganJamesSmith#1 . I then modified them to include some more checkdoc fixes for some recent changes.

I now know it'd be ideal if the branch used wasn't called "master" but it doesn't look like I can fix that without opening a new pull request

[Matafou]

Nevermind. Once the PR is closed your master branch can leave its own life.

[Matafou]

@MorganJamesSmith the failed test labelled "check-doc-magic" (the other should suceed) needs a fix from your side as follows:

• make doc locally
• git status should show some changed files under directory doc. It should be only .texi I think.
• commit this files and include them in the PR.

Thanks again!.

[hendriktews]

* ` make doc` locally

No, please do make -C doc magic in the root directory of the repository.

The manual contains literal copies of some variable and function documentation. The magic goal will copy your chnages into the texi sources of the manual. And then, as Pierre said, please include these changes in your PR.

[MorganJamesSmith]

Thanks for the instruction. I've added another commit. Let me know if that resolves everything

[hendriktews]

All tests pass now, thanks!

[Matafou]

Many thanks!