1) ppmetasenv and ppcontext to reduce the amount of printed information during

1) ppmetasenv and ppcontext to reduce the amount of printed information during
   debugging
2) BUG FIXED: boxes (in particular out_scope ones) could happear in the
   substitution after unification. In particular, this happened when the goal
   had the form   H: False |- C  and we tried to "nelim H". After the
   unification, some meta ?1 was instantiated with ?os where ?os := C. This
   triggered a unification C =?= ?1 before the end of the tactic (hence
   before the apply_subst). As a result, the ad-hoc unification case for
   in_scope/out_scope was triggered on inputs of the bad shape and an assert
   false was raised.