-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)
- | NCic.Fixpoint (ind,fl,attrs) ->
- let fl =
- List.map
- (function (relevance,name,recno,ty,bo) ->
- relevance,name,recno,apply_subst subst [] ty,apply_subst subst [] bo
- ) fl
- in
- NCic.Fixpoint (ind,fl,attrs)
- | _ -> assert false (* not implemented yet *)
-;;
+(* ============= 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