Removing a hack which, according to the comment, should not be necessary
anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
New simplification of code for generalizing hypotheses in destruct.
Not using an (arbitrary) pivot anymore for re-introduction of
quantified hypothesis in functional induction. This has apparently no
visible effect, probably because functional schemes do not have
non-dependent hypothesis in their branches besides induction
hypotheses which are anyway introduced at the top of the context.
Simplifying code of functional induction.
Further simplifying functional induction.
Test for closed #2713 and #2876.
In setoid_rewrite error messages:
- removed the encapsulation in a Tactic Failure (I don't see why
  setoid_rewrite should specifically raise a Fail - do I miss something?)
- avoid having twice a "Unable to satisfy ... constraints" message.
Removing superfluous newlines in setoid_rewrite error message.
Attempt to organize and document unification flags of setoid rewrite.
Specific printer of Evar.Set.t for ocamldebug + more information in
a UserError to ease debugging.