Experimental localization of errors during refinement and disambiguation.

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

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 7e207e12fd7970f742daed95357c959d784dbb5e..64cd5563b1d691d6035b54c03f03607f35b976fb 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -28,7 +28,8 @@ open MatitaTypes
 (** raised when ambiguous input is found but not expected (e.g. in the batch
   * compiler) *)
 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
 type choose_interp_callback = (string * string) list list -> int list