From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- pretyping/unification.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fabe24ef..5fb8054f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 9217 2006-10-05 17:31:23Z notin $ *) +(* $Id: unification.ml 9517 2007-01-22 17:37:58Z herbelin $ *) open Pp open Util @@ -113,16 +113,15 @@ let unify_0 env sigma cv_pb mod_delta m n = | LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN | _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c) - | App (f1,l1), App (f2,l2) -> - if - isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) - then + | App (f1,l1), _ when + isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) -> solve_pattern_eqn_array curenv f1 l1 cN substn - else if - isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) - then + + | _, App (f2,l2) when + isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) -> solve_pattern_eqn_array curenv f2 l2 cM substn - else + + | App (f1,l1), App (f2,l2) -> let len1 = Array.length l1 and len2 = Array.length l2 in let (f1,l1,f2,l2) = -- cgit v1.2.3