CHANGELOG

Version 2.7
* Fixed a unification bug concerning lowering of logic variables in let-head
  position.

Version 2.6
* Fixed unification issue with eta-contraction at monadic type.
* Simplified the implementation of eta-contraction and pattern substitution
  recognition to not use type information.
* Fixed issue concerning reuse of constant names (starting with "-").
* Cleaned up the error reporting infrastructure and improved error messages to
  include line numbers.
* Source code restructuring: Added phantom types to distinguish pattern
  substitutions, pattern substitutions with undefs, and general substitutions.
* Source code restructuring: Moved NatSets to their own module.
* Switched context datastructure from ML lists to Okasakis random access lists.
* Fixed non-termination bug in the unification problem
  {let {1} = c1 in let {1} = X in 1} == {let {1} = c2 in let {1} = X in 1}.
* Attached error printing information to constraints.
* Added fix for common ml-yacc / sml/nj compilation manager mismatch error to
  the README.
* Disabled the "double ctx instantiation" error, since the case correctly
  occurs after eta-expansion of a logic variable of type A&B.
  TODO: Perhaps simply disable eta-expansion instead?