Silence compilation warning by avoiding some deprecated constructs.
Ensure locality modifiers are properly highlighted in CoqIDE.
Remove a useless hypothesis from Rle_Rinv.
Silence some warning about references in documentation.
Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.
Removing useless meta-related functions.
Add lemma derivable_pt_lim_atan.

Note: the choice of the derivative comes from derivable_pt_lim_ps_atan
rather than derivable_pt_atan.
Improved the presentation of the proof of UIP_refl_nat.
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).
Stm: remove an assertion.

In the code which indents proof scripts, you cannot assume that a single goal is closed at a time (because of dependent subgoals).

This change had been lost in the rebase over the paral-itp commits in october.
Documentation of the Derive plugin.

I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
Fix g_derive.ml4.

My bad, I forgot to fix the classification before comitting.
Missing file in commit 1fb883.

It would seem that I forgot to include the actual documentation in 1fb883. As a result, the reference manual didn't compile due to missing dependencies.