hints input is cleared from projection redexes

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 7395aa7ac7cd7679ea69f4f09ce62e4a97e3a092..b91585fbe51fe699813919511004a80ee7d877a3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -611,11 +611,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
     in
     let try_hints metasenv subst t1 t2 (* exc*) =
     (*D*) inside 'H'; try let rc =  
-(*
-      prerr_endline ("\nProblema:\n" ^
+     pp(lazy ("\nProblema:\n" ^
         NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
-        NCicPp.ppterm ~metasenv ~subst ~context t2);
-*)
+        NCicPp.ppterm ~metasenv ~subst ~context t2));
       let candidates = 
         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
@@ -643,6 +641,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                      unify rdb test_eq_only metasenv subst context x y)
                   (metasenv, subst) premises
               in
+              pp(lazy("FUNZIONA!"));
               Some (metasenv, subst)
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
             with
@@ -731,12 +730,20 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn)
      | Uncertain msg as exn -> 
-       match try_hints metasenv subst t1 t2 with
+(*
+       prerr_endline "PROBLEMA";
+       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
+       prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
+*)
+       let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in
+       match 
+         try_hints metasenv subst 
+           (NCicReduction.unwind t1) (NCicReduction.unwind t2) 
+       with
        | Some x -> x
        | None -> 
           try 
-            unif_machines metasenv subst 
-             (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
+            unif_machines metasenv subst (t1m, t2m)
           with 
           | UnificationFailure _ -> raise (UnificationFailure msg)
           | Uncertain _ -> raise exn