X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=da0cee2d4c64867b51eb6dbecfb233ce5546da3c;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=2edd1bd69c7bfdfe380a590418022008743465c0;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml
index 2edd1bd69..da0cee2d4 100644
--- 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))