From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 3 Oct 2008 14:09:28 +0000 (+0000)
Subject: better test
X-Git-Tag: make_still_working~4701
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bfb7d5f4d6c812d5c5b036da654fd4f987f69bc9;p=helm.git

better test
---

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