| T.Statement _ :: l
| T.Qed _ :: l ->
xl frm l
+ | T.Reflexivity _ :: l ->
+ F.fprintf frm "\\Reflexivity"; xl frm l
+ | T.Exact (t, _) :: l ->
+ F.fprintf frm "\\Exact{%a}" xat t; xl frm l
| T.Intros (_, [r], _) :: l ->
F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
| T.LetIn (r, v, _) :: l ->