X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FandOrTree.ml;h=57be10271ded62c906900763a4b97d80f2f72097;hb=00da35cbf619e0d1f3d7fde7e6a0e6e4dc6c0915;hp=22d36844fbc5583200eb3338be31d0bfb99ec2f1;hpb=3c77b701737ef41c39a5d08d76ca9071e5b1bdd7;p=helm.git

diff --git a/helm/software/components/ng_tactics/andOrTree.ml b/helm/software/components/ng_tactics/andOrTree.ml
index 22d36844f..57be10271 100644
--- a/helm/software/components/ng_tactics/andOrTree.ml
+++ b/helm/software/components/ng_tactics/andOrTree.ml
@@ -61,6 +61,14 @@ let downO p =
     | Node(`And s,[]) -> Solution s
     | _ -> assert false
 
+let downOr p = 
+ match downr p with
+ | Some x -> Todo x
+ | None -> 
+    match eject p with
+    | Node(`And s,[]) -> Solution s
+    | _ -> assert false
+
 let left = left
 let right = right