Change the interface of proof_global to take an evar_map instead of a universe context to start proofs.

It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
Proof_global.start_dependent_proof: properly threads the sigma through the telescope.

Allows for a more refined notion of dependently generated initial goals.
Proof_global: an unused variable replaced by a wildcard.
When closing a proof, make sure that the types have their evar substituted.

When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
Derive plugin: a more general interface.

Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.
Derive plugin: small refactoring.
Derive plugin: code reorganisation for clarity.
Derive plugin: add some comments.
Derive plugin: document new syntax.