From e81c7a0e24d24ab71685fbc46f7e7e2c2f02c495 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Dec 2008 13:53:16 +0000 Subject: [PATCH] make it compile again --- helm/software/components/ng_refiner/check.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2