| Shift, _ -> fail (lazy "can't shift goals here")
| Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
when is_fresh loc ->
| Shift, _ -> fail (lazy "can't shift goals here")
| Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
when is_fresh loc ->