X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.mli;h=7e207e12fd7970f742daed95357c959d784dbb5e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=740de989ecfa027c3c73a0e1f63c8355b1f7dafd;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 740de989e..7e207e12f 100644
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -28,6 +28,7 @@ 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
 
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = (string * string) list list -> int list
@@ -48,7 +49,3 @@ val mono_interp_callback: choose_interp_callback
 (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
 
 include Disambiguate.Disambiguator
-  (*
-   * val disambiguate_term: ...
-   *)
-