]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicUnification.ml
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml
index 9ee056aed4f6a6911ea11c658bafe4873c019494..bfa1388a98b965d0489b34aebbff4721b0e714df 100644 (file)
@@ -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 *)