From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 May 2009 21:45:30 +0000 (+0000)
Subject: Bug fixed: the relevance list can be shorted then leftno args.
X-Git-Tag: make_still_working~3992
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a767bbd80be1d253e00d6b450d8205de142cc9c2;p=helm.git

Bug fixed: the relevance list can be shorted then leftno args.
---

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