refactoring for TFF1 in progress
Basic.Sym introduced for a simple representation of symbols,
used by the parser and AST
Symbol.t is now typed (symbols are equal if same name and same type)
added module DBEnv (substitutions for De Bruijn)
Type.Forall constructor, now with De Bruijn indices, and efficient
Type.apply function to provide type arguments
FOTerm.Node has a list of type arguments before its
term arguments
HOTerm with type arguments and better De Bruijn handling
updated FOFormula with better De Bruijn handling;
expose some DB internals in FOTerm and HOTerms, but with warnings
updated unification and substitution
Signature no longer maps symbols to types, but
strings to (typed) symbols
continue the refactoring that annotates symbols and applications with type arguments
updated tests, tools, arbitrary and meta prover
bugfixes in logtk
bugfix in type inference
fix some tests and updated .ocamlinit
unsuccessful attempt to make the meta prover work;

this will require more work and more thought about how explicit
polymorphism and meta-prover should go along.
update type erasure so that free type vars can be quantified;
functions to compute the set of free type variables in terms and formulas;
type_check now can print the annotated set of input formulas (function to do that in Util_tptp)
ocamldoc errors fixed