X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=cc103a8ab6036349cf5893da12a0076773b49cc6;hb=4ab08405286d0e1409893ee6477ac4686bacf103;hp=1f03755ffbd9cde673cc3be5c9cbeffe9809d23f;hpb=511421f12dd04547bbf1206470e5d39237673429;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 1f03755ff..cc103a8ab 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -50,7 +50,7 @@ let eta_reduce subst t =
           let _,_,t,_ = NCicUtils.lookup_subst i subst in
           let t = NCicSubstitution.subst_meta lc t in
           eat_lambdas ctx t
-        with Not_found -> ctx, t)
+        with NCicUtils.Subst_not_found _ -> ctx, t)
     | t -> ctx, t
   in
   let context_body = eat_lambdas [] t in
@@ -572,12 +572,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              (NCicTypeChecker.typeof ~metasenv ~subst context meta)
           in
           let metasenv, subst = 
-           try
-            unify rdb test_eq_only metasenv subst context 
-              (C.Meta (i,l)) lambda_Mj swap
-           with UnificationFailure msg | Uncertain msg when not norm2->
-            (* failure: let's try again argument vs argument *)
-            raise (KeepReducing msg)
+           unify rdb test_eq_only metasenv subst context 
+            (C.Meta (i,l)) lambda_Mj swap
           in
           let metasenv, subst = 
             unify rdb test_eq_only metasenv subst context t1 t2 swap
@@ -612,8 +608,6 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              with
                 Invalid_argument _ -> 
                  raise (Uncertain (mk_msg metasenv subst context t1 t2))
-              | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
-                 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
               | KeepReducing _ | KeepReducingThis _ -> assert false
            in 
              metasenv, subst
@@ -660,7 +654,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
        | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
     in
+    let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
+     try fo_unif test_eq_only metasenv subst nt1 nt2
+     with
+      UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+       raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+    in
     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
+      if NCicUntrusted.metas_of_term subst context t1 = [] &&
+         NCicUntrusted.metas_of_term subst context t2 = [] 
+      then None 
+      else begin
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^
         ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
@@ -701,6 +705,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
       in
         cand_iter candidates
      (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+      end
     in
     let put_in_whd m1 m2 =
       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,