X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=59bc5d7e72ef9f11ee048545d11c616d367e2820;hb=156b87c397a8b5cf9b7381def41e070e235941ee;hp=22f896f21e12c13fa26fe2cb5d6133911385481a;hpb=4b6193be548c96964beee706b75a06e269eed88d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 22f896f21..59bc5d7e7 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -86,7 +86,7 @@ let pp s =
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
 ;;  
 
-(* let pp _ = ();; *)
+let pp _ = ();;
 
 let fix_sorts swap metasenv subst context meta t =
   let rec aux () = function
@@ -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
@@ -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;;