better test

[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 0f92a18a3ff6d45d46e79cfc0765b4536c5e4a79..3a155329e679ba235f2c5da77987ae69455b96c4 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -66,6 +66,7 @@ let mk_cprop n =
 
 
 let _ =
+  Sys.catch_break true;
   let do_old_logging = ref true in
   HelmLogger.register_log_callback
    (fun ?append_NL html_msg ->
@@ -209,8 +210,8 @@ let _ =
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
           let ctx, ty = intros ty in
-          let ity =
-            match ity with
+          let whd ty =
+            match ty with
             | NCic.Appl [eq;t;a;b] ->
                NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
             | t -> NCicReduction.whd ~delta:0 ctx t
@@ -224,7 +225,7 @@ let _ =
           let metasenv, subst = 
             try 
 (*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity sty 
+              NCicUnification.unify menv [] ctx ity (whd sty) 
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg