From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 6 Apr 2009 15:50:28 +0000 (+0000)
Subject: eta-contraction was made on the wrong term
X-Git-Tag: make_still_working~4114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86ff79af764c2a434fdf38ea344ab722811981c8;p=helm.git

eta-contraction was made on the wrong term
---

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d64fb005f..006fcafe1 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -317,11 +317,11 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
                   (C.Meta (i,l)) lambda_Mj
               in
               let t1 = NCicReduction.whd ~subst context t1 in
-              let i, l = 
+              let j, lj = 
                 match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
               in
               let metasenv, subst = 
-                instantiate hdb test_eq_only metasenv subst context i l t2 true
+                instantiate hdb test_eq_only metasenv subst context j lj t2 true
               in
               (try
                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in