- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 3000b7311dca621bcedfc3464380621c13d3e2a6..09d9ede475cd12bc1a88e34fbf5be307527f1024 100644 (file)
--- 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))
@@ -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 "NU 2" lno relevance)
+                  with Failure _ -> []
+                 in
                    HExtlib.mk_list false lno @ relevance
              | _ -> relevance
            in
@@ -612,8 +615,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
  (*D*)  in outside(); rc with exn -> outside (); raise exn 
 ;;
 
-let unify hdb = 
+let unify hdb ?(test_eq_only=false) = 
   indent := "";      
-  unify hdb false;;
-
-
+  unify hdb test_eq_only;;