1) improved (???) debugging, with

1) improved (???) debugging, with
  1.1 more messages (good)
  1.2 messages for exceptions (very good)
  1.3 vim folding/unfolding (good or very bad?)
2) bug partially fixed (to be improved/totally fixed):
   when we unify a ?n:? vs a term t, we need to check
   that t is a sort! (or a flexible term??? what to do in that case?)
   otherwise we can get ?n := O and ?1:?2:?n=0 which is a not
   well typed metasenv. Hence boom later.