Matitaweb:

[helm.git] / matitaB / components / disambiguation / multiPassDisambiguator.ml

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml
index 2edd1bd69c7bfdfe380a590418022008743465c0..da0cee2d4c64867b51eb6dbecfb233ce5546da3c 100644 (file)
--- a/matitaB/components/disambiguation/multiPassDisambiguator.ml
+++ b/matitaB/components/disambiguation/multiPassDisambiguator.ml
@@ -166,7 +166,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   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
@@ -174,5 +174,8 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
       ~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))