Test fixed by PMP's commits from Oct 21.
Test #3655 was failing due to an anomaly. Now it rather has to fail
normally, so failure is now detected by removing the "Fail".
Compatibility with 8.4 in the heuristic used to build the induction
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
Continuing 3741c46fe134 on reporting ltac error.
- Do use the flag for_ml for distinguishing coq level and ml level
  ltac definitions.
- Skip ML call from the trace.

There are still differences from 8.4 and trunk. For instance on:

Ltac f x := refine x.
Goal False.
f I.

8.4 says:

In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".

trunk says:

In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".

Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:
One missing evar was making the whole substitution fail.
The bug actually existed a priori also in the case where only metas
are substituted (i.e. before bcba6d1bc9f769da), leading to limit the
number of situations where it could be effectful.

This fixes current failures of RelationAlgebra and CFGV.
Follow up to experimental eager evar unification in bcba6d1bc9:

Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).