error...

[helm.git] / helm / software / components / ng_refiner / check.ml

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 4adff1569d3051721352c6de92ee3e7be387d370..1d3408d6b4b1d64c135cb72449a8d37394eccd05 100644 (file)
--- 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