More cleanup/reorganizing of univ.ml to separate constraint/universe handling from
the instance/contexts and substitution code.