X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=1d3408d6b4b1d64c135cb72449a8d37394eccd05;hb=e8fb6062a3c126dc242ee7bc44a696d73ca8ed76;hp=4adff1569d3051721352c6de92ee3e7be387d370;hpb=761aef3c864626e17004b9785c39def7053271e0;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 4adff1569..1d3408d6b 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -210,9 +210,20 @@ let _ =
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
           let ctx, ty = intros ty in
+          let ity =
+            match ity with
+            | NCic.Appl [eq;t;a;b] ->
+               NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
+            | t -> t
+          in
+                prerr_endline 
+                 (Printf.sprintf "%s == %s"
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
           let metasenv, subst = 
             try 
-              NCicUnification.unify menv [] ctx ity sty
+                    prerr_endline ("INIZIO: " ^ NUri.string_of_uri u);
+              NCicUnification.unify menv [] ctx ity sty 
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg