A Type Checker for the exported files
We have written a type-checker (almost finished)
for the exported files to be sure that all the interesting information
was exported
The type-checker is used to check either theories or
single objects
Objects are not checked in the "static"
environment in which they were defined. An environment is dinamically
created during type-checking: when the t.c. finds a reference to
a not yet checked object, this one is recursively checked first.