X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FzipTree.mli;h=6a6c4d67f4a51d3dbb1ef937eb664680c319ba10;hb=7daf77fac7dc562c3b0a363c7bf4f84d39de4280;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..6a6c4d67f 100644
--- a/helm/software/components/ng_tactics/zipTree.mli
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -11,4 +11,34 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val repeat : ('a -> 'a option) -> 'a -> 'a
+
+module type Elem = sig type t val pp : t -> string end ;;
+
+module type ZipTree = sig
+  type t
+  type tree = Node of (t * tree) list
+  type position
+
+  val start : tree -> position
+
+  val up    : position -> position option
+  val down  : position -> position option
+  val left  : position -> position option
+  val right : position -> position option
+
+  val root: position -> tree
+  val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
+
+  val get: position -> t
+  val set: t -> position -> position
+
+  val inject: tree -> position -> position
+  val eject: position -> tree
+
+  val dump: position -> Format.formatter -> unit
+
+end
+
+module Make(T : Elem) : ZipTree with type t = T.t