- lowtac_status ->
- found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
- postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
- cic_term -> ast_term option * NCic.term ->
- lowtac_status * cic_term
+ #pstatus as 'status ->
+ found: ('status -> cic_term -> 'status * cic_term) ->
+ postprocess: ('status -> cic_term -> 'status * cic_term) ->
+ cic_term -> tactic_term option * NCic.term ->
+ 'status * cic_term
+
+val mk_in_scope: #pstatus as 'status -> cic_term -> 'status * cic_term
+val mk_out_scope:
+ int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term
+
+val pp_status: #pstatus -> unit
+
+class ['stack] status :
+ NCic.obj -> 'stack ->
+ object ('self)
+ inherit pstatus
+ method stack: 'stack
+ method set_stack: 'stack -> 'self
+ end
+
+class type lowtac_status = [unit] status
+
+type 'status lowtactic = #lowtac_status as 'status -> int -> 'status