Experimental localization of errors during refinement and disambiguation.

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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 0f4dc67db6b9fafc977d414b3f7e85f5a79b729e..d46f9a1bfbefd5b059623adabfa65dbab046cfbd 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,7 +28,8 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
-exception DisambiguationError of string Lazy.t list list
+exception DisambiguationError of
+ (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list