Moved unif to elab, corrected bugs in the elaboration of constraints, better interface for conv and expr, start unification.