(C.Meta (i,l)) lambda_Mj,
i
| NCic.Meta (i,_) -> (metasenv, subst), i
- | _ -> prerr_endline ("XXX: " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.whd ~subst context t1)); assert false
+ | _ ->
+ raise (UnificationFailure (lazy "Locked term vs non
+ flexible term; probably not saturated enough yet!"))
in
let t1 = NCicReduction.whd ~subst context t1 in
let j, lj =