s, t
;;
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let _,context,t = t in
+ NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
let disambiguate status t ty context =
let status, expty =
match ty with
;;
let mk_cic_term c t = None,c,t ;;
+
+let apply_subst status ctx t =
+ let status, (name,_,t) = relocate status ctx t in
+ let _,_,_,subst,_ = status.pstatus in
+ status, (name, ctx, NCicUntrusted.apply_subst subst t)
+;;