+ '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
+
+class type ['stack] g_status =
+ object
+ inherit g_pstatus
+ method stack: 'stack
+ end
+
+class ['stack] status :
+ NCic.obj -> 'stack ->
+ object ('self)
+ inherit pstatus
+ method stack: 'stack
+ method set_stack: 'stack -> 'self
+ method set_status: 'stack #g_status -> 'self
+ end
+
+class type lowtac_status = [unit] status
+
+type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
+
+class type tac_status = [Continuationals.Stack.t] status
+
+val pp_tac_status: #tac_status -> unit
+
+type 'status tactic = #tac_status as 'status -> 'status
+
+(* indexing facilities over cic_term based on inverse De Bruijn indexes *)
+
+module NCicInverseRelIndexable : Discrimination_tree.Indexable
+with type input = cic_term and type constant_name = NUri.uri
+
+module Ncic_termSet : Set.S with type elt = cic_term