- | `Coercion -> "coercion"
- | `Elim Cic.Prop -> "elimProp"
- | `Elim Cic.CProp -> "elimCProp"
- | `Elim Cic.Set -> "elimSet"
- | `Elim (Cic.Type _) -> "elimType"
- | `Record -> "record"
- | `Projection -> "projection"
+ | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+ | `Elim s ->
+ Xml.xml_nempty "class" [None,"value","elim"]
+ [< Xml.xml_empty
+ "SORT" [None,"value",
+ (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
+ None,"id","elimination_sort"] >]
+ | `Record field_names ->
+ Xml.xml_nempty "class" [None,"value","record"]
+ (List.fold_right
+ (fun name res ->
+ [< Xml.xml_empty "field" [None,"name",name]; res >]
+ ) 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"]