From 48a389fa5b4c7d80f97c8c6c7a1f47e840977f39 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Nov 2010 11:45:10 +0000 Subject: [PATCH] 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). --- .../components/ng_refiner/nCicUnification.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) 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 -- 2.39.2