- metasenv, (env, todo, left)::tail
- | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
- assert (L.length tl >= 1);
- metasenv, ([g1], [], [])::(tl, todo, left)::tail
- | Branch, (_, _) -> raise (Error "can't branch on a singleton context")
- | Shift opt_pos, (metasenv, (leftopen, t, l)::(goals, todo, left)::tail) ->
+ proof, (env, todo, left, tag)::tail
+ | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
+ assert (List.length tl >= 1);
+ proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
+ | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
+ | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
+ (goals, todo, left,tag)::tail) ->