-(*
- let goal,mustdot =
- let s = status#stack in
- match s with
- | [] -> fail (lazy "Invalid use of done")
- | (g1, _, k, tag1) :: tl ->
- let goals = filter_open g1 in
- let (loc::tl) = goals in
- let goal = goal_of_loc (loc) in
- if List.length k > 0 then
- goal,true
- else
- goal,false
- in
-
- *)
-(*
- let goals = filter_open g1 in
- let (loc::tl) = goals in
- let goal = goal_of_loc (loc) in
- if tag1 == `BranchTag then
- if List.length (shift_goals s) > 0 then (* must simply shift *)
- (
- prerr_endline (pp status#stack);
- prerr_endline "Head goals:";
- List.map (fun goal -> prerr_endline (string_of_int goal)) (head_goals status#stack);
- prerr_endline "Shift goals:";
- List.map (fun goal -> prerr_endline (string_of_int goal)) (shift_goals status#stack);
- prerr_endline "Open goals:";
- List.map (fun goal -> prerr_endline (string_of_int goal)) (open_goals status#stack);
- if tag2 == `BranchTag && g2 <> [] then
- goal,true,false,false
- else if tag2 == `BranchTag then
- goal,false,true,true
- else
- goal,false,true,false
- )
- else
- (
- if tag2 == `BranchTag then
- goal,false,true,true
- else
- goal,false,true,false
- )
- else
- goal,false,false,false (* It's a strange situation, there's is an underlying level on the
- stack but the current one was not created by a branch? Should be
- an error *)
- | (g, _, _, tag) :: [] ->
- let (loc::tl) = filter_open g in
- let goal = goal_of_loc (loc) in
- if tag == `BranchTag then
-(* let goals = filter_open g in *)
- goal,false,true,false
- else
- goal,false,false,false
- in
- *)