+
+let apply_subst status ctx t =
+ let status, (name,_,t) = relocate status ctx t in
+ 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)
+;;