Need documentation of pretyping/elaboration error messages

[jfehrle]

At least one of the ~20 pretyping error messages is not documented. They should all be documented and probably as a group in their own subsection. The doc should mention the term "pretyping" in the glossary and relate it to "elaboration". "elaboration" should be in the glossary.

See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/error.20message.2C.20product.20vs.2E.20lambda/near/260552782