From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 Nov 2010 12:53:27 +0000 (+0000)
Subject: Back-porting from new matita:
X-Git-Tag: make_still_working~2679
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9078eadc955930e7e37cfc2451a40416512c95fa;p=helm.git

Back-porting from new matita:

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/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index dd1e4b80c..e2f6a7090 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/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