X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=120d3e9cb4b43f3582dd698d4616928cfb43bad5;hb=62f476a05884d451bfb90d845ea2b1c0a1c77f96;hp=7d13b9a35df112e7a76d5441203d2dae77dbf129;hpb=53be448c4f8ca0b60be92e24f355662a0ea7567f;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 7d13b9a35..120d3e9cb 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -226,6 +226,8 @@ let _ =
                  (fun e ctx -> e::ctx) ctx perforate metasenv t
           in
           let rec curryfy ctx = function
+            | NCic.Lambda (name, (NCic.Sort _ as s), tgt) ->
+                NCic.Lambda (name, s, curryfy ((name,NCic.Decl s) :: ctx) tgt)
             | NCic.Lambda (name, s, tgt) ->
                 let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
                 NCic.Lambda (name, NCic.Implicit `Type, tgt)
@@ -269,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