This PR rewords the `application type mismatch` error message by more
specifically mentioning that the problem is with the final argument.
This is useful when the same argument is passed to the function multiple
times.
We decided against using a wording which specifically mentions the
"function expression", because users who are not used to currying might
not think of the `f a` in `f a b` as a function.
This PR enables the elaboration of theorem bodies, i.e. proofs, to
happen in parallel to each other as well as to other elaboration tasks.
Specifically, to be eligible for parallel proof elaboration,
* the theorem must not be in a `mutual` block
* `deprecated.oldSectionVars` must not be set
* `Elab.async` must be set (currently defaults to `true` in the language
server, `false` on the cmdline)
To be activated for downstream projects (i.e. in stage 1) pending
further Mathlib validation.
This PR adds an addition newline before the "Additional diagnostic
information may be available using the `set_option ... true` command."
messages, to provide better visual separation from the main error
message.
