better test

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 22c0881aa26c66160610e37fe0f1b4abce6b82c3..3a155329e679ba235f2c5da77987ae69455b96c4 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -210,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
@@ -225,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