let rec render_step sep a = function
| Note s -> mk_note s :: a
| Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a
- | Qed s -> mk_note s :: mk_qed :: a
+ | Qed s -> (* mk_note s :: *) mk_qed :: a
| Id s -> mk_note s :: cont sep (mk_id :: a)
| Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
| Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)