fixed coercions undoooing

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 03e50588f4b98cea91c45a1d39ade776440f2b64..ed739eefbebb8c9be4a9e5ab95f919166625a722 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -607,7 +607,9 @@ class gui () =
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
-        (fun exn ->
+        (function 
+        | MatitaScript.ActionCancelled -> () 
+        | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
            let floc, msg = MatitaExcPp.to_string exn in
             begin