diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
| commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
| tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /pretyping/unification.ml | |
| parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) | |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 17 |
1 files changed, 8 insertions, 9 deletions
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) = |