X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=5500abcbf189ee44073a288ac59049410b4cd083;hb=48a389fa5b4c7d80f97c8c6c7a1f47e840977f39;hp=9227289c6808f73fb6abf2e7bf725ce7854c876f;hpb=95b2fec522138b2a17e6f8ddc71683eb9dbf3413;p=helm.git

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 9227289c6..5500abcbf 100644
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -575,17 +575,21 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
             * function even in the easy case above *)
            let easy_case = 
              match t2 with
-             | NCic.Appl (f :: f_args)  
-               when List.length args = List.length f_args && 
+             | NCic.Appl (f :: f_args)
+               when 
                List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
+                let mlen = List.length args in
+                let flen = List.length f_args in
+                let min_len = min mlen flen in
+                let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+                let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
                  (try 
-                    let metasenv, subst = 
-                      unify rdb test_eq_only metasenv subst context meta f swap
-                    in
                     Some (List.fold_left2 
                       (fun (m, s) t1 t2 -> 
-                        unify rdb test_eq_only m s context t1 t2 swap)
-                        (metasenv, subst) args f_args)
+                        unify rdb test_eq_only m s context t1 t2 swap
+                      ) (metasenv,subst)
+                        ((NCicUntrusted.mk_appl meta mhe)::margs)
+                        ((NCicUntrusted.mk_appl f fhe)::fargs))
                   with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
                     None) 
              | _ -> None