From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 2 Oct 2009 17:55:03 +0000 (+0000)
Subject: hints input is cleared from projection redexes
X-Git-Tag: make_still_working~3395
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1a0d19ddcb2682947ef610f8634cc80c134b558;p=helm.git

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 7395aa7ac..b91585fbe 100644
--- 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