Changes to disambiguation:

Changes to disambiguation:

* bug fixed: when pruning from the disambiguation domain symbols with
  just one interpretation, not all of them were pruned
* improvement: errors due to symbols with no interpretation are now
  immediately detected

Changes to refinement:

* major improvement:
  one error was always raised as an Uncertain; it is now raised as a
  Failure when it is the case (i.e. a term/type is found where a sort is
  expected and the term/type has no flexible head).
  This bug fix exponentially decrease the number of refinements performed
  in the disambiguation of some terms in ASM/Status.ma in CerCo