unification hints with recursive calls do work!

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index a0cda6861c512ef8e31e0974a14af5d7768457ad..55ccca12a0c79dc16fc84180af3dab442dc66bb3 100644 (file)
--- 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