From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Dec 2008 13:53:16 +0000 (+0000)
Subject: make it compile again
X-Git-Tag: make_still_working~4384
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e81c7a0e24d24ab71685fbc46f7e7e2c2f02c495;p=helm.git

make it compile again
---

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 120d3e9cb..7fbb781df 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -272,11 +272,12 @@ let _ =
           (try 
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof 
-                ~look_for_coercion:(fun _ _ _ _ _ -> []) [] [] [] bo None
+                ~look_for_coercion:(fun _ _ _ _ _ -> [])
+               NCicUnifHint.empty_db  [] [] [] bo None
             in
             let metasenv, subst = 
               try 
-                NCicUnification.unify metasenv subst [] infty ty
+                NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty
               with
               | NCicUnification.Uncertain msg 
               | NCicUnification.UnificationFailure msg