From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 3 Feb 2004 14:10:53 +0000 (+0000)
Subject: catch just AssertFailure instead of _ (AssertFailure is the only
X-Git-Tag: V_0_2_3~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44f465fa4b07556033c5c6c196a52cf16599589c;p=helm.git

catch just AssertFailure instead of _ (AssertFailure is the only
exception that could be raised there since the invoked function wraps
every exception inside it)
---

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 70c7aa9cb..1dc4ae2bd 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -106,7 +106,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
             type_of_aux' metasenv' subst'' context t
           in
            fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
-        with _ ->
+        with AssertFailure _ ->
           (* TODO huge hack!!!!
            * we keep on unifying/refining in the hope that the problem will be
            * eventually solved. In the meantime we're breaking a big invariant: