coercions are there, but not heavily tested

[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 d4a329697d667287d859b03e58150cc8d7f93a39..120d3e9cb4b43f3582dd698d4616928cfb43bad5 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -271,7 +271,8 @@ let _ =
           let bo = curryfy [] bo in
           (try 
             let metasenv, subst, bo, infty = 
-              NCicRefiner.typeof [] [] [] bo None
+              NCicRefiner.typeof 
+                ~look_for_coercion:(fun _ _ _ _ _ -> []) [] [] [] bo None
             in
             let metasenv, subst = 
               try