This version of disambiguate.ml implements yet another (better?) criterio for

spurious error detection. An error is spurious iff:

a) it is obtained interpreting a symbol s using an interpretation \phi
b) there exists another interpretation \phi' such that
   1) dom(\phi') = dom(\phi)
   2) \phi' is valid

It should be true that no nested error locations should occur.
In principle this also suggests the possibility of changing the user interface
to show all alternative errors at the same time.