From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 1 Sep 2009 08:25:33 +0000 (+0000)
Subject: catch wrapped exception
X-Git-Tag: make_still_working~3515
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=544a9aee8a26a4d7c613ef8a02f045c53d55f998;p=helm.git

catch wrapped exception
---

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 035e65ac7..25beed259 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -239,8 +239,8 @@ let select_term
     (* we could lift wanted step-by-step *)
     try true, unify status ctx (None, ctx, t) wanted
     with 
-    | NCicUnification.UnificationFailure _ 
-    | NCicUnification.Uncertain _ -> false, status
+    | Error (_, Some (NCicUnification.UnificationFailure _))
+    | Error (_, Some (NCicUnification.Uncertain _)) -> false, status
   in
   let match_term status ctx (wanted : cic_term) t =
     let rec aux ctx (status,already_found) t =