X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=3a155329e679ba235f2c5da77987ae69455b96c4;hb=bfb7d5f4d6c812d5c5b036da654fd4f987f69bc9;hp=22c0881aa26c66160610e37fe0f1b4abce6b82c3;hpb=5563af448ba05dcfac528b56b67baf333cfca000;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 22c0881aa..3a155329e 100644
--- 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