(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