(** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
* choice from the user is needed to disambiguate the term
(** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
* choice from the user is needed to disambiguate the term