+
+let apply_subst status ctx t =
+ let status, (name,_,t) = relocate status ctx t in
+ let _,_,_,subst,_ = status#obj in
+ status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)
+;;
+
+(* ============= move this elsewhere ====================*)
+
+class ['stack] status =
+ fun (o: NCic.obj) (s: 'stack) ->
+ object
+ inherit (pstatus o)
+ val stack = s
+ method stack = stack
+ method set_stack s = {< stack = s >}
+ end
+
+class type lowtac_status = [unit] status
+
+type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
+
+class type tac_status = [Continuationals.Stack.t] status
+
+type 'status tactic = #tac_status as 'status -> 'status
+