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.