coq+vscode: Properly align suggestions.

[pimotte]

Currently, behaviour with respect to suggestions that can be inserted/copied is not that consistent. For example, the Help tactic gives suggestions inline to the text, and Expand the definition gives four lines which can all be copied or inserted, which is not relevant at all.

Proposed solution:

Adapt coq-waterproof such that we clearly communicate what a message is:

• A suggestion (insertable)
• An error/warning (copiable)
• Exposition (neither)

Acceptation criteria:

• All tactics in coq-waterproof clearly communicate intend with messages
• The vscode side properly uses these to decide which buttons to show