- 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)::tail
+ | Branch, (proof, (g1::tl, todo, left)::tail) ->
+ assert (List.length tl >= 1);
+ proof, ([g1], [], [])::(tl, todo, left)::tail
+ | Branch, (_, _) -> fail "can't branch on a singleton context"
+ | Shift opt_pos, (proof, (leftopen, t, l)::(goals, todo, left)::tail) ->