- let _,_,_,subst,_ = status.pstatus in
- let rec aux ctx =
- function
- NCic.Meta (i,lc) ->
- (try
- let _,_,t,_ = NCicUtils.lookup_subst i subst in
- let t = NCicSubstitution.subst_meta lc t in
- aux ctx t
- with
- Not_found ->
- match lc with
- _,NCic.Irl _ -> NCic.Meta (i,lc)
- | n,NCic.Ctx l ->
- NCic.Meta
- (i,(0,NCic.Ctx
- (List.map (fun t -> aux ctx (NCicSubstitution.lift n t)) l))))
- | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx aux t
- in
- status, (name, ctx, aux ctx t)
+ let _,_,_,subst,_ = status#obj in
+ status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)