+ | T.LetIn (r, v, _) :: l ->
+ F.fprintf frm "\\Pose{%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 "\\Change{%a}{%s}{%a}" xat u (quote s) xl l
+ | T.Rewrite (b, t, None, _, _) :: l ->
+ F.fprintf frm "\\Rewrite{%s}{%a}{}{}{%a}" (xh b) xat t xl l
+ | T.Rewrite (b, t, Some (s1, Some s2), _, _) :: l ->
+ F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
+ (xh b) xat t (quote s1) (quote s2) xl l
+ | T.Rewrite (b, t, Some (s1, None), _, _) :: l ->
+ F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
+ (xh b) xat t (quote s1) (quote s1) xl l
+ | T.Apply (t, _) :: T.Branch (ls, _) :: l ->
+ let z = num (List.length ls) in
+ F.fprintf frm "\\%sApply{%a}%a" z xat t xls ls; xl frm l
+ | T.Apply (t, _) :: l ->
+ F.fprintf frm "\\Apply{%a}{%a}" xat t xl l
+ | T.Cases (v, _, _) :: T.Branch (ls, _) :: l ->
+ let z = num (List.length ls) in
+ F.fprintf frm "\\%sCases{%a}%a" z xat v xls ls; xl frm l
+ | T.Cases (v, _, _) :: l ->
+ F.fprintf frm "\\Cases{%a}{%a}" xat v xl l
+ | T.Elim (v, Some t, _, _) :: T.Branch (ls, _) :: l ->
+ let z = num (List.length ls) in
+ F.fprintf frm "\\%sElim{%a}{%a}{}{}%a" z xat v xat t xls ls; xl frm l
+ | T.Elim (v, Some t, _, _) :: 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.Inductive _ :: _ -> assert false
+ | T.Id _ :: _ -> assert false
+ | T.Clear _ :: _ -> assert false
+ | T.ClearBody _ :: _ -> assert false
+ | T.Branch _ :: _ -> assert false
+ | T.Intros _ :: _ -> 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)
+