explanations for add contraction/weakening etc. unification interface barely documented, needs a code cleanup(huet unification is commented out completely, but it wouldnt fit the interface etc). removed parsing/hlk and added the necessary part into shlk.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2315 85d21ef8-add0-11de-ae77-5bfb9c5a3f34