+
+ | NCic.Appl (NCic.Meta (i,l)::args), NCic.Meta (n, _) when
+ not (NCicMetaSubst.flexible subst args) &&
+ is_locked n subst &&
+ not (List.mem_assoc i subst)
+ ->
+ (* we verify that none of the args is a Meta,
+ since beta expanding w.r.t a metavariable makes no sense *)
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args
+ in
+ let metasenv, subst =
+ unify hdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj
+ in
+ let t1 = NCicReduction.whd ~subst context t1 in
+ let i, l =
+ 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
+ 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)