(** {2 Goal stack} *)
+(* Key value pairs *)
+type parameters = (string * string) list
+
module Stack:
sig
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 entry = locator list * locator list * locator list * tag * parameters
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 of_nmetasenv: (goal * 'a) list -> t
val head_switches: t -> switch list (** top level switches *)
val head_goals: t -> goal list (** top level goals *)