| C.AImplicit _ -> assert false
| C.AAppl (_, []) -> assert false
-and xats frm vs =
- let map v = F.fprintf frm "{%a}" xat v in
- List.iter map vs
+and xats frm = function
+ | [] -> F.fprintf frm "{}"
+ | vs ->
+ let map v = F.fprintf frm "{%a}" xat v in
+ List.iter map vs
in
xat frm t
| 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 ->
F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
+ | T.LApply (r, v, _) :: l ->
+ F.fprintf frm "\\LApply{%a}{%a}{%a}" xx r xat v xl l
| T.Change (u, _, None, _, _) :: l ->
F.fprintf frm "\\Change{%a}{}{%a}" xat u xl l
| T.Change (u, _, Some (s, _), _, _) :: l ->
F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
| T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
+ | T.Record _ :: _ -> assert false
| T.Inductive _ :: _ -> assert false
| T.Id _ :: _ -> assert false
| T.Clear _ :: _ -> assert false
| T.Elim _ :: _ -> assert false
| T.Cut _ :: _ -> assert false
-and xls frm ls =
- let map l = F.fprintf frm "{%a}" xl l in
- List.iter map (List.rev ls)
+and xls frm = function
+ | [] -> F.fprintf frm "{}"
+ | ls ->
+ let map l = F.fprintf frm "{%a}" xl l in
+ List.iter map (List.rev ls)
in
F.fprintf frm "%a@\n" xl l