huge commit regarding the grafite_status:

[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 7d1e20a4d65cb67ba656b07c83e133204dd7c53d..5f4d8d150d0cff31f3e2dbe3018d6553412b186e 100644 (file)
--- 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                                ->
@@ -225,6 +231,7 @@ let rec xl frm = function
       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.Record _ :: _                                       -> assert false
    | T.Inductive _ :: _                                    -> assert false
    | T.Id _ :: _                                           -> assert false
    | T.Clear _ :: _                                        -> assert false
@@ -234,9 +241,11 @@ let rec xl frm = function
    | 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)
+and xls frm = function
+   | [] -> F.fprintf frm "{}"
+   | ls -> 
+      let map l = F.fprintf frm "{%a}" xl l in
+      List.iter map (List.rev ls)
 
 in
 F.fprintf frm "%a@\n" xl l