nicer (but convertible) types

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 22819536fe31b02ea993b8cf3dcc6185c549b5d2..325e290a74f4636d231d136b2b2f2995808cc597 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,6 +28,9 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int * (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
@@ -79,8 +82,8 @@ let disambiguate_thing ~aliases ~universe
 =
   assert (universe <> None);
   let library = false, DisambiguateTypes.Environment.empty, None in
-  let multi_aliases=false, DisambiguateTypes.Environment.empty, universe in
-  let mono_aliases = true, aliases, None in
+  let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+  let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
   let passes =  (* <fresh_instances?, aliases, coercions?> *)
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
@@ -103,18 +106,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 (offset,newerrors) ->
+          raise (DisambiguationError (offset, errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)
-        with Disambiguate.NoWellTypedInterpretation -> aux tl)
+        with Disambiguate.NoWellTypedInterpretation (_offset,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 ->