1) sort computation undone (it used to be bugged anyway)

[helm.git] / helm / software / components / ng_tactics / andOrTree.ml

diff --git a/helm/software/components/ng_tactics/andOrTree.ml b/helm/software/components/ng_tactics/andOrTree.ml
index 22d36844fbc5583200eb3338be31d0bfb99ec2f1..57be10271ded62c906900763a4b97d80f2f72097 100644 (file)
--- 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