+ type switch = Open of goal | Closed of goal
+ type locator = int * switch
+ type tag = [ `BranchTag | `FocusTag | `NoTag ]
+ type entry = locator list * locator list * locator list * tag
+ type t = entry list
+
+ val empty: t
+
+ val find_goal: t -> goal (** find "next" goal *)
+ val is_empty: t -> bool (** a singleton empty level *)
+ val of_metasenv: Cic.metasenv -> t
+ val head_switches: t -> switch list (** top level switches *)
+ val head_goals: t -> goal list (** top level goals *)
+ val head_tag: t -> tag (** top level tag *)
+ val shift_goals: t -> goal list (** second level goals *)
+ val open_goals: t -> goal list (** all (Open) goals *)
+ val goal_of_switch: switch -> goal
+
+ (** @param int depth, depth 0 is the top of the stack *)
+ val fold:
+ env: ('a -> int -> tag -> locator -> 'a) ->
+ cont:('a -> int -> tag -> locator -> 'a) ->
+ todo:('a -> int -> tag -> locator -> 'a) ->
+ 'a -> t -> 'a
+
+ val iter: (** @param depth as above *)
+ env: (int -> tag -> locator -> unit) ->
+ cont:(int -> tag -> locator -> unit) ->
+ todo:(int -> tag -> locator -> unit) ->
+ t -> unit
+
+ val map: (** @param depth as above *)
+ env: (int -> tag -> locator list -> locator list) ->
+ cont:(int -> tag -> locator list -> locator list) ->
+ todo:(int -> tag -> locator list -> locator list) ->
+ t -> t
+
+ val pp: t -> string
+end
+
+(** {2 Functorial interface} *)
+
+module type Status =
+sig
+ type input_status
+ type output_status
+