New behaviour of fo_unif: in case of ?f args == t args'

where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 9227289c6808f73fb6abf2e7bf725ce7854c876f..5500abcbf189ee44073a288ac59049410b4cd083 100644 (file)
--- 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