fix convertibility in case of application test_eq_only is =true for

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

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 120d3e9cb4b43f3582dd698d4616928cfb43bad5..4e85f9bae069d64214ccb599d4d9579e6e83f62c 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -193,7 +193,7 @@ let _ =
     | NCicTypeChecker.TypeCheckerFailure s
     | NCicEnvironment.ObjectNotFound s
     | NCicEnvironment.BadConstraint s
-    | NCicEnvironment.BadDependency s as e -> 
+    | NCicEnvironment.BadDependency (s,_) as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
     )
@@ -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