Many changes

[helm.git] / matita / components / ng_tactics / continuationals.mli

diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli
index 293d056b34e30ef7b29413ee8aeb6990454fc711..d3fdf716c895d7a86b3c58ac01b79d8e4684a17f 100644 (file)
--- a/matita/components/ng_tactics/continuationals.mli
+++ b/matita/components/ng_tactics/continuationals.mli
@@ -29,19 +29,21 @@ type goal = int
 
 (** {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 *)