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 d64fb005fe79805781ca0a79a10030d492ca2e8a..006fcafe144f61d48c8c1713b4876c8d24420669 100644 (file)
--- 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