+
+let map_obj_kind f =
+ function
+ NCic.Constant (relev,name,bo,ty,attrs) ->
+ NCic.Constant (relev,name,HExtlib.map_option f bo, f ty,attrs)
+ | NCic.Fixpoint (ind,fl,attrs) ->
+ let fl =
+ List.map
+ (function (relevance,name,recno,ty,bo) -> relevance,name,recno,f ty,f bo)
+ fl
+ in
+ NCic.Fixpoint (ind,fl,attrs)
+ | NCic.Inductive (is_ind,lno,itl,attrs) ->
+ let itl =
+ List.map
+ (fun (relevance,name,ty,cl) ->
+ let cl =
+ List.map (fun (relevance, name, ty) ->
+ relevance, name, f ty)
+ cl
+ in
+ relevance, name, f ty, cl)
+ itl
+ in
+ NCic.Inductive (is_ind,lno,itl,attrs)
+;;
+
+let apply_subst subst t =
+ let rec apply_subst subst () =
+ function
+ NCic.Meta (i,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst i subst in
+ let t = NCicSubstitution.subst_meta lc t in
+ apply_subst subst () 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 ->
+ apply_subst subst () (NCicSubstitution.lift n t)) l))))
+ | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
+ in
+ apply_subst subst () t
+;;
+