X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTeX.ml;h=279ebecb99982bf1cd48b9b19cce54a6a8bdad47;hb=ef05c795559108c1d33cfa048531849807867a81;hp=55be4ddb3f17168c41c8bb3ee7c8ab17b0cf77dc;hpb=592b7d81b57ec66e0ee007de336e249b07ae0258;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml index 55be4ddb3..279ebecb9 100644 --- a/helm/software/components/acic_procedural/proceduralTeX.ml +++ b/helm/software/components/acic_procedural/proceduralTeX.ml @@ -194,6 +194,8 @@ let rec xl frm = function | T.Statement _ :: l | T.Qed _ :: l -> 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 ->