X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=59bc5d7e72ef9f11ee048545d11c616d367e2820;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=f178fc4b780f824143bd19af4cb2dca2b85b52fb;hpb=0542386e10041791982e7240f281299677b1997b;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index f178fc4b7..59bc5d7e7 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -417,7 +417,10 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
            let relevance = NCicEnvironment.get_relevance r1 in
            let relevance = match r1 with
              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
-                 let _,relevance = HExtlib.split_nth lno relevance in
+                 let relevance =
+                  try snd (HExtlib.split_nth lno relevance)
+                  with Failure _ -> []
+                 in
                    HExtlib.mk_list false lno @ relevance
              | _ -> relevance
            in