- | Note s -> mk_notenote s a
- | Theorem (n, t, s) -> mk_theorem n t :: mk_thnote s a
- | Qed s -> mk_qed :: mk_tacnote s a
- | Id s -> mk_id sep :: mk_tacnote s a
- | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a
- | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a
- | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
- | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
- | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
- | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a
- | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a
- | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a
- | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps sep a ps
- | Branch (ps :: pss, s) ->
+ | Note s -> mk_notenote s a
+ | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a
+ | Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a
+ | Qed s -> mk_qed :: mk_tacnote s a
+ | Exact (t, s) -> mk_exact t sep :: mk_tacnote s a
+ | Id s -> mk_id sep :: mk_tacnote s a
+ | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a
+ | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a
+ | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
+ | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
+ | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
+ | Cases (t, e, s) -> mk_cases t e sep :: mk_tacnote s a
+ | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a
+ | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a
+ | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a
+ | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps sep a ps
+ | Branch (ps :: pss, s) ->