a few missing ~subst added to whd

[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 bb423690b177a2865aae6b19914822e555ffa61f..120d3e9cb4b43f3582dd698d4616928cfb43bad5 100644 (file)
--- 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 
@@ -282,7 +285,7 @@ let _ =
                   metasenv, subst
               | Sys.Break -> metasenv, subst
             in
-            if (NCicReduction.are_convertible ~subst [] infty ty)
+            if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
             then
               prerr_endline ("OK: " ^ NUri.string_of_uri u)
             else
@@ -308,11 +311,16 @@ let _ =
               NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
             in*)
           with
+          | Sys.Break -> ()
           | NCicRefiner.RefineFailure msg 
           | NCicRefiner.Uncertain msg ->
              let _, msg = Lazy.force msg in
              prerr_endline msg;
-             prerr_endline ("FAIL: " ^ NUri.string_of_uri u))
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+          | e -> 
+             prerr_endline (Printexc.to_string e); 
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+             )
       | _ -> ())
     alluris;
 ;;