]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_procedural/proceduralTeX.ml
1) the home button of CicBrowser now works also for NG
[helm.git] / helm / software / components / acic_procedural / proceduralTeX.ml
index 55be4ddb3f17168c41c8bb3ee7c8ab17b0cf77dc..402ef54fe7d2a03e0ee72c3ec6c74f8557ff7d74 100644 (file)
@@ -194,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                                ->