X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;fp=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=b8a3dd44a0af3340efe48830192578eaf3060a32;hb=4400d6a1bf09682b3c679edf0e1775117fe059c2;hp=29341cb5dd72b3dcf6abd7d7e38d1d7c0a7e3142;hpb=2dee545ec9874703b954b57c3b4c300f6cf3b8a2;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 29341cb5d..b8a3dd44a 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -267,6 +267,7 @@ let solve f status eq_cache goal =
                         Lazy.force msg ^
 			"\n in the environment\n" ^ 
 			status#ppmetasenv subst metasenv)); None
+      | Sys.Break as e -> raise e
       | _ -> None
     in
     HExtlib.filter_map build_status
@@ -436,7 +437,9 @@ let close_metasenv status metasenv subst =
            (* prerr_endline (status#ppterm ctx [] [] iterm); *)
            let s_entry = i, ([], ctx, iterm, ty)
            in s_entry::subst,okind::objs
-         with _ -> assert false)
+         with
+            Sys.Break as e -> raise e
+          | _ -> assert false)
       (subst,[]) metasenv
 ;;