X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fcontinuationals.mli;h=d3fdf716c895d7a86b3c58ac01b79d8e4684a17f;hp=1dcf4aa7dc8fcc2a61af433ec7bb661a42520e32;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hpb=9ab5bcc58aa62e4ded71fd64cc5a4ea562195103

diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli
index 1dcf4aa7d..d3fdf716c 100644
--- a/matita/components/ng_tactics/continuationals.mli
+++ b/matita/components/ng_tactics/continuationals.mli
@@ -29,12 +29,15 @@ 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