X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=759f630b4b8abaa0100bac5ff1695ad789ec2e98;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 3be3ba7f1..759f630b4 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -260,8 +260,22 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-  (* TODO ZACK implement attributes pretty printing *)
-let xml_of_attrs attributes = [< >]
+let xml_of_attrs attributes =
+  let class_of = function
+    | `Coercion -> "coercion"
+    | `Elim Cic.Prop -> "elimProp"
+    | `Elim Cic.CProp -> "elimCProp"
+    | `Elim Cic.Set -> "elimSet"
+    | `Elim (Cic.Type _) -> "elimType"
+    | `Record -> "record"
+    | `Projection -> "projection"
+  in
+  let xml_attr_of = function
+    | `Generated -> None, "generated", "true"
+    | `Class c -> None, "class", class_of c
+  in
+  let xml_attrs = List.map xml_attr_of attributes in
+  Xml.xml_empty "attributes" xml_attrs
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let find_sort id =