Matitaweb: first attempt at web UI for disambiguation.

[helm.git] / matitaB / components / disambiguation / disambiguate.mli

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index bb20ff86635ca1ec53a6b218b610c7f36b97f2a7..2e6677d727f7996bf60b813363b78079c4c1b95f 100644 (file)
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -25,10 +25,6 @@
 
 (** {2 Disambiguation interface} *)
 
-(** 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 *)
 (* list of located error messages, each list is a tuple:
   * - environment in string form
@@ -58,6 +54,7 @@ type ('term,'metasenv,'subst,'graph) test_result =
 
 exception Try_again of string Lazy.t
 
+(*
 val set_choose_uris_callback:
   DisambiguateTypes.interactive_user_uri_choice_type -> unit
 
@@ -76,6 +73,7 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
   * choose_interp_callback if not set otherwise with set_choose_interp_callback
   * above *)
 val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+*)
 
 val resolve : 
   env:'alias1 DisambiguateTypes.InterprEnv.t ->