Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.

This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.

With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.

To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.

Closes GH-557.

* Lastly, package-menu-async keeps its initial value even if we C-g.

* require package.el (in a safe way thanks to `proof-try-require`)

Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.

After 574b09 92e3cb4b7a4ad88400b9a5ab0198a96ca5, make magic fails
with a recursive require chain. No requires were changed in that
commit, it's unclear to me, why there is no recursive require
chain with (eval-when (compile).