fix

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 3c0d1b4c359ba15ba418b70f1cd74585a6d27484..619c1eadbbd5e229f3394baf883fc3b3a8367ecc 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -26,8 +26,6 @@
 exception PopupClosed
 open Printf
 
-open MatitaTypes
-
 let wrap_callback f = f
 
 let connect_button (button: #GButton.button) callback =
@@ -340,7 +338,6 @@ let ask_confirmation ~title ~message ?parent () =
     !rc
 
 let report_error ~title ~message ?parent () =
-  let rc = ref false in
   let callback _ = () in
   let buttons = GWindow.Buttons.ok in
   try 
@@ -392,7 +389,7 @@ let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false)
   connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
   dialog#emptyDialog#show ();
   GtkThread.main ();
-  (match !result with None -> raise Cancel | Some r -> r)
+  (match !result with None -> raise MatitaTypes.Cancel | Some r -> r)
 
 type combo_status = Free of string | Locked of string