- | [p] -> render_step None a p
- | (Note _ | Theorem _ | Qed _ as p) :: ps ->
- render_steps (render_step None a p) ps
- | p :: ((Branch ([], _) :: _) as ps) ->
- render_steps (render_step None a p) ps
+ | [p] -> render_step sep a p
+ | p :: Branch ([], _) :: ps ->
+ render_steps sep a (p :: ps)