Removed 'typ' and used 'term' also for type terms

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/new_prover.ml
	modified:   ocaml/proof.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
	modified:   ocaml/term_table.ml
	deleted:    ocaml/type.ml
Term unification now symmetric

Given two terms 't1' and 't2' and a number of variables 'nvars' the algorithm finds a substitution for the
variables so that none of the variables occurs in the substitution terms and that the substitution applied
to 't1' and 't2' makes them identical. In case that no substitution exists the algorithm raises 'Not_found'.
This symmetric version of the unification is necessary in order to apply it within the type checker.

Fix: There has been a bug in the function 'sub'. The substitution terms have to be shifted up by 'nb' in case
that the substitution happens in an environment with 'nb' bound variables.

Optimization: The functions 'upbound' and 'up' check if the number of shifts is zero. In this case nothing
has to be done, i.e. the algorithm is applied only to shifts above zero.

	modified:   ocaml/term.ml
First step to make symmetric unification incremental

The substitution consisting of an array of terms and an array of flags has been factored out in
order to make unification incremental.

	modified:   ocaml/term.ml
Fix: removed 'open Type'

The module 'type.ml' does not exist anymore

	modified:   ocaml/assertion_table.mli
Added the module 'Option'

	modified:   ocaml/container.ml
Added some more syntatic types

	modified:   ocaml/class_table.ml
Added signature maps to find features

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Simplified 'has_value' to 'has' in module 'Option'

	modified:   ocaml/container.ml
Made the module 'Term.Sub' publicly available

	modified:   ocaml/term.ml
Added a draft version of the type checker with type inference

A datatype 'context' with a global context (class_table, featura_table, assertion_table, ...)
and stack local context has been added to the system which is already partially in use.

The type checker has not yet been activated, just included into the package.

	modified:   library/kernel/boolean.e
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/makefile
	new file:   ocaml/signature.ml
	modified:   ocaml/support.ml
	modified:   ocaml/term.ml
	new file:   ocaml/typer.ml
	renamed:    local_context.ml -> local_ass_context.ml
	renamed:    local_context.mli -> local_ass_context.mli
	modified:   prover.ml
	new file:   ocaml/context.ml
Clean up of 'eiffelc.ml'

The parsing of arguments is now done in a separate function and not
in the main function of 'eiffelc.ml'.

	modified:   ocaml/eiffelc.ml
All global tables now used exclusively via Context.t

	modified:   ocaml/context.ml
	modified:   ocaml/eiffelc.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/prover.mli
	modified:   ocaml/support.ml
Some streamlining in the analysis of signatures

- function type eliminated
- formal generic names used consistently in some functions

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/signature.ml
Added procedure flag into Sign.t

	modified:   ocaml/signature.ml
Used 'type_term' instead of 'term' if the term describes a type

	modified:   ocaml/class_table.ml
Improved the analysis of syntactic signatures

- collection of the number of untyed variables (because they need
  type variables) and adding corresponding type variables to the
  signature

- introduced 'Sign.t' into the analysis functions

- removed some unnecessary functions

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/signature.ml
Added the pushing of contexts

	modified:   ocaml/context.ml
	modified:   ocaml/signature.ml

	modified:   ocaml/eiffelc.ml
Feature definitions simplified

The argument names and types are already included in the feature descriptor.
Therefore they have been dropped from the definition.

	modified:   ocaml/feature_table.ml
Added formal generic names to classes and the function 'type2string'

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
Completed the draft of the type checking algorithm

	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/typer.ml