disambiguate_thing ~description_of_alias ~passes ~aliases
~universe ~visit ~f thing
*)
- try
+ match
Disambiguate.disambiguate_thing
~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context
~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
~mk_localization_tbl ~pp_term thing
with
- | Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, [newerrors]))
+ | Disambiguate.Disamb_success res -> res
+ | Disambiguate.Disamb_failure (herrors, serrors) ->
+ (* temporary *)
+ let offset = 0 in
+ raise (DisambiguationError (offset, newerrors))