X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FzipTree.mli;h=751d3720dd61a01b2375cc9c0a8ca339b27f2ffa;hb=ef6a409b9cea2a3d0b0852ae3e69737566c91ba1;hp=04e9a7b7c8313fc9ece05b71e37d25a32801c86a;hpb=315f37e0c47d4af8c1767b4f836d74c7125ab736;p=helm.git

diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli
index 04e9a7b7c..751d3720d 100644
--- a/helm/software/components/ng_tactics/zipTree.mli
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -11,4 +11,28 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil 
+type ('a,'s,'g) position
+
+val start : ('s,'g) tree -> ('a,'s,'g) position
+
+val up    : ('a,'s,'g) position -> ('b,'s,'g) position option
+val down  : ('a,'s,'g) position -> ('b,'s,'g) position option
+val downr : ('a,'s,'g) position -> ('b,'s,'g) position option
+val left  : ('a,'s,'g) position -> ('b,'s,'g) position option
+val right : ('a,'s,'g) position -> ('b,'s,'g) position option
+
+val is_top :  ('a,'s,'g) position -> bool
+
+val root: ('a,'s,'g) position -> ('s,'g) tree
+
+val get: ('a,'s,'g) position -> 's * 'g
+val set: 's -> 'g -> ('a,'s,'g) position -> ('a,'s,'g) position
+
+val inject: ('s,'g) tree -> ('a,'s,'g) position -> ('a,'s,'g) position
+val eject: ('a,'s,'g) position -> ('s,'g) tree
+
+val dump: ('g -> string) -> ('s -> string -> Format.formatter -> unit) -> 
+            ('a,'s,'g) position -> Format.formatter -> unit
+