- Procedural: now we generate the exact tactic (in place of some apply tactics) and...

[helm.git] / helm / software / components / acic_procedural / proceduralTeX.ml

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index 55be4ddb3f17168c41c8bb3ee7c8ab17b0cf77dc..279ebecb99982bf1cd48b9b19cce54a6a8bdad47 100644 (file)
--- 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                                ->