Included formal generics info into 'TVars'

The module 'TVars' contains now then names and the concepts of the formal
generics beside the local type variables and the global type variables
imported from global features. Therefore 'TVars' together with the class table
provides a complete context for any type term, i.e. the triple (tp,tvars,ct)
defines a unique type in the type system.

With this type context the function 'Class_table.satisfies' is now more simple.

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   context.ml
	modified:   context.mli
	modified:   feature_table.ml
	modified:   signature.ml
	modified:   term.ml
	modified:   term_builder.ml
Removed some unnecessary functions

	modified:   signature.ml
Improved error message

In case that an expression does not satisfy any of the expected types then
possible actual types are printed as well in the error message.

	modified:   typer.ml
Removed a dummy argument which caused confusion

	modified:   context.ml
	modified:   context.mli
	modified:   typer.ml
Used TVars in feature table

instead of 'fgnames' and 'concepts'

	modified:   feature_table.ml
	modified:   signature.ml
Used TVars now consistently to specify a local type context

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   context.ml
	modified:   feature_table.ml
	modified:   feature_table.mli
Ownership calculation simplified

Each signature is owned by a class. Since all class indices and all
module indices are now nonnegative integers the ownership calculation
could be simplified.

In order to calculate the ownership of a signature one has to compute
the set of all involved classes. The class with the highest module
rank is the owner of the signature.

Not yet implemented: Modules with multiple classes!!

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   feature_table.ml
	modified:   signature.ml
Minor editorial changes

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   context.ml
	modified:   signature.ml
Concepts of type variables (formal generics) no longer absolute

'TVars.t' is a context for types and contains the number of free type
variables, for each globally imported (from the feature table) type variable a
concept and for each formal generic of the context a concept.

Up to now the concepts have been absolute. Therefore they could not refer to
other type variables in the type context.

Now all concepts (of imported or local type variables) are relative to the
type context. With this adaption concepts of type variables can refer to other
type variables.

With this relativeness we can define formal generics which depend on other
formal generics.

Example:

    G: ANY

    deferred class ABSTRACT_ARRAY[G] ... end

    AA[G]: ABSTRACT_ARRAY[G]    -- not yet accepted by the parser

    size(a:AA[G]): NATURAL      deferred end

    [] (a:AA[G], i:NATURAL): G
        require
            i < a.size
        deferred end

    put(a:AA[G], i:NATURAL, v:G)
        require
             i < a.size
        deferred ensure
             a[i] = v
        end

	modified:   class_table.ml
	modified:   context.ml
	modified:   context.mli
	modified:   feature_table.ml
	modified:   signature.ml
	modified:   term_builder.ml
Factored out the TVars module into a separate file

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   context.ml
	modified:   context.mli
	modified:   feature_table.ml
	modified:   feature_table.mli
	modified:   signature.ml
	modified:   term_builder.ml
	modified:   term_builder.mli
	new file:   tvars.ml
	new file:   tvars.mli
	modified:   typer.ml
Added documentation

	modified:   tvars.mli
Added the function 'TVars.is_equal'

The function 'is_equal tp1 tvs1 tp2 tvs2' compares the two types 'tp1'
and 'tp2' which come from different environments 'tvs1' and 'tvs2'. Two
types are considered equal if they have the same classes in the same
positions of the type term or both a type variable in the same position
and their corresponding concepts are equal.

	modified:   tvars.ml
Fix: Discharged term must be transformed to the local environment

The prover might encounter the fact that the current goal has already
been proved in some outer environment. Before discharging this term
with the local assumptions and all-quantifying it, the term has to
be transformed into the local environment.

This bug has not been detected up to now because in the most cases the
discharged term is from the local environment.

	modified:   proof_table.ml
Finding of variant features implemented

A descendant class can effect of redefine features from a ancestor class.
These features are called variants of the original feature.

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   feature_table.ml
	modified:   support.ml
	modified:   tvars.ml
	modified:   tvars.mli
Seeds and variants implemented in feature table

Initially each feature is its own seed and has no variants.

If a feature is inherited in a descendant, then the inherited feature
inherits all seeds from the feature and is no longer its own seed
and all seeds of the feature have the feature in the descendant as
a variant.

	modified:   feature_table.ml
Tvars.principal_class implemented

The function finds the principal class of a type term.

	modified:   feature_table.ml
	modified:   tvars.ml
	modified:   tvars.mli
'Term_builder.update_term' implemented and used for inheritance

The term builder finds first the most general term using e.g.
deferred features. The function 'update_term' checks if there is a
more specific feature in the descendant class and uses this if
possible instead of the most general feature.

The most specific features do not appear in the feature map. Therefore
only the most general features (i.e. the seeds) are found first. The
update procedure finds the correct variant.

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/term_builder.mli
	modified:   ocaml/term_table.ml
	modified:   ocaml/term_table.mli
	modified:   ocaml/typer.ml
Inheritance of effective features implemented

If a class implements all deferred features of an ancestor class then
it inherits all effective features of the class. During inheritance
the type environment and the definition term must be update appropriately.

Redefinition of features not yet implemented.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/signature.ml
	modified:   ocaml/term.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/tvars.ml
	modified:   ocaml/tvars.mli
Fix: calculation of the class index in 'Class_table.get_type'

The calculation of the class index has not been done correctly in the
presence of type variables.

	modified:   ocaml/class_table.ml
	modified:   ocaml/typer.ml
Fix: 'Term_sub_arr.remove_bottom'

Substitutions of the removed type variables not done correctly.

	modified:   ocaml/signature.ml
	modified:   ocaml/typer.ml