X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=3ca6a3a5040990370f722c0e8c30755b1a1eba3d;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=056240ef13899e24b08a8adf1b9aac306f94eb64;hpb=05feb31551afc1eafd1d350c3facc23fdda5bebe;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 056240ef1..3ca6a3a50 100644
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -276,9 +276,18 @@ let xml_of_attrs attributes =
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
   in
+  let flavour_of = function
+    | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
+    | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
+    | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
+    | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
+    | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+  in
   let xml_attr_of = function
     | `Generated -> Xml.xml_empty "generated" []
     | `Class c -> class_of c
+    | `Flavour f -> flavour_of f
   in
   let xml_attrs =
    List.fold_right