λδ site update

[helm.git] / helm / software / components / ng_tactics / zipTree.mli

diff --git a/helm/software/components/ng_tactics/zipTree.mli b/helm/software/components/ng_tactics/zipTree.mli
index 04e9a7b7c8313fc9ece05b71e37d25a32801c86a..751d3720dd61a01b2375cc9c0a8ca339b27f2ffa 100644 (file)
--- 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
+