X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=24a8355237b7d1e4a7b81d4b58068a01537bc22d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=cd4d42420de20f6ddc815d7bbbaa80a60f43955f;hpb=b12aa2f7dc56d9915603339e9a1e1ba23d834b4a;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index cd4d42420..24a835523 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,6 +28,7 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
+exception DisambiguationError of string Lazy.t list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
@@ -103,18 +104,23 @@ let disambiguate_thing ~aliases ~universe
    else
     drop_aliases_and_clear_diff res
   in
-  let rec aux =
+  let rec aux errors =
     function
-    | [ pass ] -> set_aliases pass (try_pass pass)
+    | [ pass ] ->
+        (try
+          set_aliases pass (try_pass pass)
+         with Disambiguate.NoWellTypedInterpretation newerrors ->
+          raise (DisambiguationError (errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)
-        with Disambiguate.NoWellTypedInterpretation -> aux tl)
+        with Disambiguate.NoWellTypedInterpretation newerrors ->
+         aux (errors @ [newerrors]) tl)
     | [] -> assert false
   in
   let saved_use_coercions = !CoercDb.use_coercions in
   try
-    let res = aux passes in
+    let res = aux [] passes in
     CoercDb.use_coercions := saved_use_coercions;
     res
   with exn ->
@@ -135,10 +141,10 @@ type disambiguator_thing =
  }
 
 let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
   { do_it =
      fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
-     -> profiler.CicUtil.profile
+     -> profiler.HExtlib.profile
          (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
            ~drop_aliases_and_clear_diff) thing
   }