Primitive definitions, intervals and Arend coercion, confluence for conditions, proper absurd patterns, proper holes and pattern unification, new expressions for records (support a very naive binding technique), records with conditions, LaTeX backend, internal refactoring