X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FzipTree.ml;h=30f09940ed7acc4229377de190e2b1d7a8eb2323;hb=6dd2a996e8443d57fa3e3d0988829d01485d838a;hp=45c7f02b94b595d4029be769afee73418fe0bf36;hpb=da715664068e859d20ab81fd6969e64d58c0f57e;p=helm.git

diff --git a/helm/software/components/ng_tactics/zipTree.ml b/helm/software/components/ng_tactics/zipTree.ml
index 45c7f02b9..30f09940e 100644
--- a/helm/software/components/ng_tactics/zipTree.ml
+++ b/helm/software/components/ng_tactics/zipTree.ml
@@ -29,6 +29,15 @@ let down = function
   | Loc (ctx, Node (s,(x,t)::tl)) -> Some (Loc (Ctx (ctx,s,[],x,tl),t))
 ;;
 
+let downr = function 
+  | Loc (_,(Nil|Node (_,[]))) -> None
+  | Loc (ctx, Node (s,(_::_ as l))) -> 
+     match List.rev l with
+     | [] -> assert false
+     | (x,t) :: tl ->     
+         Some (Loc (Ctx (ctx,s,tl,x,[]),t))
+;;
+
 let up = function
   | Loc (Top,_) -> None
   | Loc (Ctx(ctx,s,l,x,r),t) -> Some (Loc (ctx,Node (s,(List.rev l)@[x,t]@r)))
@@ -95,7 +104,7 @@ let dump ppg pps pos fmt =
     match pos with
     | Top -> ()
     | Ctx(ctx,s,l,x,r) ->
-        let t = Node(s,l@[x,skip]@r) in
+        let t = Node(s,(List.rev l)@[x,skip]@r) in
         let cur = !c in
         aux_t t;
         incr c;
@@ -107,10 +116,11 @@ let dump ppg pps pos fmt =
         aux ctx
   in
   let Loc (ctx, t) = pos in
-  let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->l in
+  let l = match ctx with Top -> assert false | Ctx (_,_,l,_,_)->List.rev l in
   let cur = !c in
   Pp.node ("node"^string_of_int !c) 
     ~attrs:["style","filled";"fillcolor","red";"color","red"] fmt;
+  Pp.edge  ("node"^string_of_int !c)  ("node"^string_of_int !c) fmt;
   aux_t t;
   incr c;
   Pp.edge