From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 May 2012 08:11:13 +0000 (+0000)
Subject: Sys.Break no longer captured in two places.
X-Git-Tag: make_still_working~1762
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4400d6a1bf09682b3c679edf0e1775117fe059c2;p=helm.git

Sys.Break no longer captured in two places.
---

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
 ;;