update in groud_2 and models

[helm.git] / helm / software / matita / matitaGui.mli

diff --git a/helm/software/matita/matitaGui.mli b/helm/software/matita/matitaGui.mli
index 388c79e1a74dd903372c72716dd7da57d191e6bb..796c33fef4b9fb42559561d91b61422816f3ea43 100644 (file)
--- a/helm/software/matita/matitaGui.mli
+++ b/helm/software/matita/matitaGui.mli
@@ -43,10 +43,10 @@ val interactive_uri_choice:
   ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
   ?ok_action:[`AUTO|`SELECT] ->
   ?copy_cb:(string -> unit) -> unit ->
-    GrafiteDisambiguator.choose_uris_callback
+  id:'a -> UriManager.uri list -> UriManager.uri list
 
   (** @raise MatitaTypes.Cancel *)
 val interactive_interp_choice:
   unit ->
-    GrafiteDisambiguator.choose_interp_callback
+    DisambiguateTypes.interactive_interpretation_choice_type