added Variant theorem flavour

[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 056240ef13899e24b08a8adf1b9aac306f94eb64..3ca6a3a5040990370f722c0e8c30755b1a1eba3d 100644 (file)
--- 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