Adding a test for bug #2923.
Simplifying interface of elimination tactics. They used dummy clausenvs, and
that should be changed anyway.
Small code cleaning in Tacticals.
Removing tactic compatibility layer from Elim.
Using the new monad tactic in Inv.
Removing the compatibility layer from Leminv. Also removed an undocumented
variant of the Derive Inversion command which took the current goal as the
targeted inductive. It was unused in the contribs and it seemed rather
bad from the STM point of view, as it generated a lemma inside a proof.
Add regression tests for 3188 and 3265
Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Coquelicot.

This change removes the need for excluded middle. It also greatly
simplifies the proof (no need for geometric series, limits, constructive
epsilon, and so on).
Remove some uses of excluded middle.
Import proof of decidability of negated formulas from Coquelicot.
Removing dead code, thanks to new OCaml warnings and a bit of scripting.