EXPERIMENTAL:

EXPERIMENTAL:
 1. the disambiguation domain is now a tree that partially reflects the
    applicative structure of the term
 2. disambiguation now classifies errors according to the following criterium:
    an error E is considered not significant when it belongs to the set A of
    results (obtained interpreting a symbol and its subterms in every possible
    way) and there exists at least a result in A that is either OK or Uncertain.
    A "subterm" is implicitly defined by the tree structure of the
    disambiguation domain.
 3. WARNING: there used to be an (important ????) optimization that has not
    been ported (yet ???): if the next item in the disambiguation domain can
    be interpreted in just one way, we skip the current refinement step.
    According to tests on my laptop the optimization does not seem to be
    really so significant (sometimes it even slow down???). We will decide
    on monday whether porting it or not. Porting it is not very simple because
    of the new data structures involved.