Fixing a bug in the presence of let-in in inductive arity.
A patch for printing "match" when constructors are defined with let-in
but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.
Fixing a (new) part of bug #2729.

By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.

This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.

Another part is still open (see test-suite).
Removing re-typecheking from "refine" in no-check mode of the new
convert_concl/convert_hyp. This was actually probably the main source
of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than
nf_enter, as suspected in 3c2723f.
Continuing experimental printing of the signature of open evars in
Check (see cfff8f8a327) [printing only visible evars, not the ones
corresponding to unrelated open goals + fixing bug on wrong sigma and
on evar_info normalization].
Dead code.
More precise test for #3459.
Adapting output tests to the removal of the new token warning and to
the printing of the context of open evars in Check.
Porting Hugo's fix 98f3abb83a to native compiler.
Adding an evar version of the make_clenv function.
Using new clausenv in rewrite.
Fixing decompose_app_rel in Rewrite.

The old implementation did not beta-iota normalize before observing the head of
the term, resulting in stange bugs.
Lazily check that an argument is dependent when constructing evar clauses.
Small invariants in Rewrite code.
Removing dead code in Rewrite.
Remove duplicate code.
Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.

As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
Remove the deprecated open-constr based refine.

That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals.

There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs.

Factored code with Ltac's refine in Extratactics.
Remove unused functions for side effects.
Proofview: factor init and dependent_init.