Allow proofs to start with dependent goals.

I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
Vernac classification: allow for commands which start proofs but must be synchrone.

The previous heuristic is to check whether the proof ends with Qed or not. This modification allows for commands which start proof but may produce transparent term even when the function ends with Qed.
The commands that initiate proofs are now in charge of what happens when proofs end.

The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it.

In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands.

In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
Refactoring: storing more information in the terminator closure.

We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.

In this commit, we remove the compute_guard parameter.
Factoring(continued).

This commit removes the hook.
Proof_global: fix start_proof comment after the preceding commits.
Fix Admitted.

Commit "The commands that initiate proofs…" was a bit hasty in its treatment of Admitted (in an attempt of making things simple, I actually required the proof to be completed for Admitted to go through…).
Derive plugin.

A small plugin to support program deriving (à la Richard Bird) in Coq.

It's fairly simple:

  Require Coq.Derive.Derive.

  Derive f From g Upto eq As h.

Produces a goal (actually two, but the first one is automatically shelved):

  |- eq g ?42

And closing the proof produces two definitions: f is instantiated with the value of ?42 (it's always transparent). And h is instantiated with the content of the proof (it is transparent or opaque depending on whether the proof was closed with Defined or Qed).