- let _,_,t,_ = List.assoc i subst in
- is_flexible status context ~subst t
- with Not_found -> true)
- | NCic.Appl (NCic.Meta (i,_) :: args)->
- (try
- let _,_,t,_ = List.assoc i subst in
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta status lc t in