unify hdb test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
- | 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
let t1 = NCicReduction.whd ~subst context t1 in
let j, lj =
- match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false
+ match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
in
let metasenv, subst =
instantiate hdb test_eq_only metasenv subst context j lj t2 true
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)
+ with Not_found -> assert false))
| C.Meta (n,lc), t ->
(try