+
+ | _, NCic.Meta (n, _) when is_locked n subst ->
+ (let (metasenv, subst), i =
+ match NCicReduction.whd ~subst context t1 with
+ | NCic.Appl (NCic.Meta (i,l)::args) when
+ not (NCicMetaSubst.flexible subst args)
+ ->
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args
+ in
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj,
+ i
+ | NCic.Meta (i,_) -> (metasenv, subst), i
+ | _ -> assert false
+ in
+ let t1 = NCicReduction.whd ~subst context t1 in
+ let j, lj =
+ match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
+ in
+ let metasenv, subst =
+ instantiate rdb test_eq_only metasenv subst context j lj t2 true
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false))