status#set_stack gstatus
;;
-let branch_tac status =
+let branch_tac ?(force=false) status =
let gstatus =
match status#stack with
| [] -> assert false
| (g, t, k, tag) :: s ->
match init_pos g with (* TODO *)
- | [] | [ _ ] -> fail (lazy "too few goals to branch")
+ | [] -> fail (lazy "empty goals")
+ | [_] when (not force) -> fail (lazy "too few goals to branch")
| loc :: loc_tl ->
([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
in
| [seq] -> assert0_tac seq
| _ ->
block_tac
- (branch_tac::
+ ((branch_tac ~force:false)::
HExtlib.list_concat ~sep:[shift_tac]
(List.map (fun seq -> [assert0_tac seq]) seqs)@
[merge_tac])