DisambiguationError exceptions (that have locations inside) are now relocated

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

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