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 f178fc4b780f824143bd19af4cb2dca2b85b52fb..59bc5d7e72ef9f11ee048545d11c616d367e2820 100644 (file)
--- 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