From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Apr 2010 19:53:31 +0000 (+0000)
Subject: catch the right exception, avoid uncaught Subst_not_found
X-Git-Tag: make_still_working~2928
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4edcf284d13d4f0f945234482fda852e7b7180c4;p=helm.git

catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 1f03755ff..d4cb7a53f 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -50,7 +50,7 @@ let eta_reduce subst t =
           let _,_,t,_ = NCicUtils.lookup_subst i subst in
           let t = NCicSubstitution.subst_meta lc t in
           eat_lambdas ctx t
-        with Not_found -> ctx, t)
+        with NCicUtils.Subst_not_found _ -> ctx, t)
     | t -> ctx, t
   in
   let context_body = eat_lambdas [] t in