X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTeX.ml;h=402ef54fe7d2a03e0ee72c3ec6c74f8557ff7d74;hb=14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea;hp=f4f25c402f813d6e5c545cdcfd13ffcacd6edfa0;hpb=89519c7b52e06304a94019dd528925300380cdc0;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index f4f25c402..402ef54fe 100644
--- a/helm/software/components/acic_procedural/proceduralTeX.ml
+++ b/helm/software/components/acic_procedural/proceduralTeX.ml
@@ -168,9 +168,11 @@ let rec xat frm = function
    | 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
@@ -192,6 +194,10 @@ let rec xl frm = function
    | 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                                ->