+ let goal_pos t goal =
+ let rec aux path = function
+ | Terms.Var _ -> []
+ | Terms.Leaf x ->
+ if B.eq t x then path else []
+ | Terms.Node l ->
+ match
+ HExtlib.list_findopt
+ (fun x i ->
+ let p = aux (i::path) x in
+ if p = [] then None else Some p)
+ l
+ with
+ | None -> []
+ | Some p -> p
+ in
+ aux []
+ (match goal with
+ | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+ | _,Terms.Predicate p,_,_ -> p)
+ ;;
+