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 70c7aa9cb17c1511394233117c8f7787c04fad38..1dc4ae2bd0f08c373e7b96d359fa7a4a9e8ac249 100644 (file)
--- 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: