From bfb7d5f4d6c812d5c5b036da654fd4f987f69bc9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 3 Oct 2008 14:09:28 +0000
Subject: [PATCH] better test

---
 helm/software/components/ng_refiner/check.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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 
-- 
2.39.2