X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=e521dd30144f7db95de3950996dd1c09cd8b54ac;hb=6c4c95026020ae9924ac652482a8a0f731719e6c;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..e521dd301 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,6 +654,12 @@ 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*) =
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^