new tacticals

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

diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli
index 91a3e495bae5eefcf04515438c320b171d954fd2..e5d0e9be907a3c5be75673ba7d8b37f82590ec79 100644 (file)
--- a/helm/matita/matitaGtkMisc.mli
+++ b/helm/matita/matitaGtkMisc.mli
@@ -137,5 +137,7 @@ val report_error:
   * for prompting the user otherwise a TextEntry widget will be
   * @return the string given by the user *)
 val ask_text:
-  gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string
+  gui:#gui ->
+  ?title:string -> ?msg:string -> ?multiline:bool -> ?default:string -> unit ->
+    string