X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=55ccca12a0c79dc16fc84180af3dab442dc66bb3;hb=1eae83d9c648acdea55d333aba67fcc252b54bea;hp=a0cda6861c512ef8e31e0974a14af5d7768457ad;hpb=dc1902ae1e458e5120af63d880dbd08255bef238;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a0cda6861..55ccca12a 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -443,9 +443,9 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
     in
     let try_hints metasenv subst t1 t2 (* exc*) =
 (*
-            prerr_endline ("\n\n\n looking for hints for : " ^ 
-              NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
-              NCicPp.ppterm ~metasenv ~subst ~context t2);
+      prerr_endline ("\nProblema:\n" ^
+        NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
+        NCicPp.ppterm ~metasenv ~subst ~context t2);
 *)
       let candidates = 
         NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
@@ -454,11 +454,15 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
         | [] -> None (* raise exc *)
         | (metasenv,(c1,c2),premises)::tl -> 
 (*
-            prerr_endline ("\n attempt: " ^ 
-              NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
-              NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " AND " ^
-              NCicPp.ppterm ~metasenv ~subst ~context c2 ^  " ==?== " ^
-              NCicPp.ppterm ~metasenv ~subst ~context t2);
+            prerr_endline ("\nProvo il candidato:\n" ^ 
+              String.concat "\n"
+                (List.map 
+                  (fun (a,b) ->
+                   NCicPp.ppterm ~metasenv ~subst ~context a ^  " =?= " ^
+                   NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
+              "\n-------------------------------------------\n"^
+              NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " = " ^
+              NCicPp.ppterm ~metasenv ~subst ~context c2);
 *)
             try 
               let metasenv,subst = 
@@ -474,7 +478,6 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
               Some (metasenv, subst)
             with
               UnificationFailure _ | Uncertain _ ->
-                prerr_endline (" <candidate fails");
                 cand_iter tl
       in
         cand_iter candidates