Restore ocamlbuild
Adding a .ocamlinit in src/ also
Remove ocamlfind dependency for now
1. 'Lam' now contains a '(id*ty) list' representing binders
   instead of 'ty list'.
2. Changed the 'tyctx' in unification code from 'ty list'
   to '(id*ty) list'. Now 'tyctx'(type context) has a unified
   form in unification and typing (i.e., '(id*ty) list').
3. Updated the test cases to accommodate changes above.
Update the term printer to handle naming hints
1. Change clauses from term*(term list) tuples to a term
that are quantified by forall binders.
2. The tactics still need the old form, as well as some
test cases. The 'clausify' function in tactics.ml get a
term*(term list) tuple from a clause

Issues to be solved:
1. Some test cases in prover and tactics break because
the order which subgoals are generated changed.
2. The names generated from clausify have a very large
index.
1. Clausify does not change the order of clauses
2. Clausify does not create fresh constants. This job
   has already been taken cared by the 'freshen_clause' function
'clausify' generate a triple (tyctx,head,body) from a term clause.
This 'tyctx' are built from prefix forall binders. 'freshen_clause' no
longer judges that a constant is a logical constant from the fact that
it is captialized. Instead, it checks if this constant is in 'tyctx'.

Definitions stil use the old method (check captalized ids) to check if
a constant is logical. This might be fixed later.

All test cases updated and passed.
Added support for hh_omega:
1. Added asynchronous and synchronous objects (sequents)
2. Updated the case and search tactics for these objects

4 test cases for HH2 break for the moment. Need to fix it later
Add another form of cut with the explicit cut object: 'cut H with {L|-A}'
This allows A to be a higher order formula instead of atomic
Parsing focused sequents

    - changed syntax from {G ; [F] |- C} to {G, [F] |- C}
    - subordination checking for focused sequents in typing
    - minor changes to the lexer and parser
Partial support for searching for sync obj sequents
1. Added support to derive sync goals from sync hypothesises
2. Support focusing on members in the 'olist' context in 'search' tactic
3. Updated the 'path' example for the changes
Normalize contexts in focused sequents
A fully higher order version of the breduce theorem
converse of the bred theorem
Updated the cut-elimination theorem to the hhw style
Updated the type-uniq examples to hhw tactics
STLC normalization proofs updated to hhw
Updated the remaining type uniqueness examples to hhw