Equality has one right parameter and thus it's elimination principle has two

[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 a74206cc3b4256833e3fec2a9b6f97f1f6da82b3..751d3720dd61a01b2375cc9c0a8ca339b27f2ffa 100644 (file)
--- a/helm/software/components/ng_tactics/zipTree.mli
+++ b/helm/software/components/ng_tactics/zipTree.mli
@@ -11,32 +11,28 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val repeat : ('a -> 'a option) -> 'a -> 'a
+type ('s,'g) tree = Node of 's * ('g * ('s,'g) tree) list | Nil 
+type ('a,'s,'g) position
 
-module type Elem = sig type t val pp : t -> string end ;;
+val start : ('s,'g) tree -> ('a,'s,'g) position
 
-module type ZipTree = sig
-  type t
-  type tree = Node of (t * tree) list
-  type 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 start : tree -> position
+val is_top :  ('a,'s,'g) position -> bool
 
-  val up    : position -> position option
-  val down  : position -> position option
-  val left  : position -> position option
-  val right : position -> position option
+val root: ('a,'s,'g) position -> ('s,'g) tree
 
-  val root: position -> tree
-  val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
+val get: ('a,'s,'g) position -> 's * 'g
+val set: 's -> 'g -> ('a,'s,'g) position -> ('a,'s,'g) position
 
-  val get: position -> t
-  val set: t -> position -> position
+val inject: ('s,'g) tree -> ('a,'s,'g) position -> ('a,'s,'g) position
+val eject: ('a,'s,'g) position -> ('s,'g) tree
 
-  val inject: tree -> position -> position
-  val eject: position -> tree
+val dump: ('g -> string) -> ('s -> string -> Format.formatter -> unit) -> 
+            ('a,'s,'g) position -> Format.formatter -> unit
 
-end
-
-module Make(T : Elem) : ZipTree with type t = T.t