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.