- | 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
+ | _, 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 hdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj,
+ i
+ | NCic.Meta (i,_) -> (metasenv, subst), i
+ | _ -> assert false
+ in