X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=7d13b9a35df112e7a76d5441203d2dae77dbf129;hb=4a72a8de2b78b7ab0d200a4bf2f197d9ce2f2a13;hp=bb423690b177a2865aae6b19914822e555ffa61f;hpb=7047b93fb9479402d0592a420ed6f624dc0beea6;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bb423690b..7d13b9a35 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -282,7 +282,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 +308,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;
 ;;