- | ([], [], [])::tail -> proof, tail
- | _ -> fail "select left some goals open")
- | Qed, (proof, [[], [], []]) -> status
- | Qed, _ -> fail "can't qed an unfinished proof"
+ | ([], [], [], SelectTag)::tail -> proof, tail
+ | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail ->
+ let env =
+ (union (open_all (map_dummy_pos t))
+ (union (open_all (map_dummy_pos l))
+ (union not_processed (List.filter is_open leftopen))))
+ in
+ proof, (env,todo,left,tag)::tail
+ | _ -> fail "can't end here")