Fixing the anomaly in bug #3045 (a filter was not type-safe in
2nd-order matching).

We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.

Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).

As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.
fix make mlidoc
Coq_makefile: Allow empty logical names

I'm not sure that coqdep and coqtop understand them correctly anyway ...
Fixup leading ./ path cleaning
Adding printer for named_context_val and Goal.goal in debugger.
A version of convert_concl and convert_hyp in new proof engine.

Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
Removing Convert_concl and Convert_hyp from Logic.
Added support for having one subgoal inheriting the name of its father in Refine.
Propagating name of goal to main subgoal in cut and conversion tactics.
Restoring plugins/xml/README erased by mistake.
No need anymore for referring to xml directory in MLINCLUDES.
Fix segfault in native compiler on int31 division.

Thanks to Yves for reporting it!
Fix bug due to shadowing a variable name in tacred
Make constrMatching and detyping more robust with respect to
expand_projection failing if an innapropriate sigma is given.
Add a "Debug Tactic Unification" option and correct the first-order
application case to expand primitive projections at the head of both
applications.
Add debug printers for projections, fix printing of evar constraints
and unsatisfiable constraints which were not done in the right environment.
Give the same argument name for the record binder of type class
projections and regular records.
Easily fixable backwards incompatibility.
Do not expand primitive projections eagerly in evarconv, but only
in cases of unification with existentials requiring it.