X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=bfa1388a98b965d0489b34aebbff4721b0e714df;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=9ee056aed4f6a6911ea11c658bafe4873c019494;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 9ee056aed..bfa1388a9 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -490,8 +490,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
         NCicPp.ppterm ~metasenv ~subst ~context t2);
 *)
       let candidates = 
-        NCicUnifHint.look_for_hint 
-          rdb.NRstatus.uhint_db metasenv subst context t1 t2
+        NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
       let rec cand_iter = function
         | [] -> None (* raise exc *)