- | 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
- | 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)
- | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
- | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
- | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
- | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
- | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a)
- | Change (t, _, w, s) -> mk_note s :: cont sep (mk_change t w :: a)
- | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a)
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps sep a ps
- | Branch (pss, s) ->
+ | 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
+ | 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)
+ | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
+ | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a)
+ | Elim (t, xu, e, s) -> mk_note s :: cont sep (mk_elim t xu e :: a)
+ | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
+ | Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a)
+ | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a)
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps sep a ps
+ | Branch (pss, s) ->