let mk_cic_term c t = None,c,t ;;
-(* CSC: next two functions to be moved elsewhere *)
-let rec apply_subst subst ctx =
- 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 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 ->
- apply_subst subst ctx (NCicSubstitution.lift n t)) l))))
- | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx (apply_subst subst) t
-;;
-
-let apply_subst_obj subst =
- function
- NCic.Constant (relev,name,bo,ty,attrs) ->
- NCic.Constant
- (relev,name,HExtlib.map_option (apply_subst subst []) bo,
- apply_subst subst [] ty,attrs)
- | _ -> assert false (* not implemented yet *)
-;;
-
let apply_subst status ctx t =
let status, (name,_,t) = relocate status ctx t in
let _,_,_,subst,_ = status.pstatus in
- status, (name, ctx, apply_subst subst ctx t)
+ status, (name, ctx, NCicUntrusted.apply_subst subst t)
;;