big changes:
- unification/matching returns either a trail or raise UnifFail;
- binders bind patterns rather than variables;
- local contexts are back (scoping mechanism inside binders);
- contexts have a gensym() ability, to get context-dependent fresh variables;
- subtleties in unify/matching since the corresponding patterns must be variants