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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 59bc5d7e7..09d9ede47 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -65,7 +65,7 @@ let eta_reduce subst t =
         | Some bo -> aux (ctx,bo))
     | (name, src)::ctx, (NCic.Appl args as bo) 
       when HExtlib.list_last args = NCic.Rel 1 -> 
-        let args, _ = HExtlib.split_nth (List.length args - 1) args in
+        let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in
         (match delift_if_not_occur (NCic.Appl args) with
         | None -> aux (ctx,NCic.Lambda(name,src, bo)) 
         | Some bo -> aux (ctx,bo))
@@ -418,7 +418,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
            let relevance = match r1 with
              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
                  let relevance =
-                  try snd (HExtlib.split_nth lno relevance)
+                  try snd (HExtlib.split_nth "NU 2" lno relevance)
                   with Failure _ -> []
                  in
                    HExtlib.mk_list false lno @ relevance