let xml_of_attrs attributes =
let class_of = function
- | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+ | `Coercion n ->
+ Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
| `Elim s ->
Xml.xml_nempty "class" [None,"value","elim"]
[< Xml.xml_empty
| `Record field_names ->
Xml.xml_nempty "class" [None,"value","record"]
(List.fold_right
- (fun (name,coercion) res ->
+ (fun (name,coercion,arity) res ->
[< Xml.xml_empty "field"
- [None,"name",if coercion then name ^ " coercion" else name];
+ [None,"name",
+ if coercion then
+ name ^ " coercion " ^ string_of_int arity
+ else
+ name];
res >]
) field_names [<>])
| `Projection -> Xml.xml_empty "class" [None,"value","projection"]
| `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
| `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
| `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+ | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
in
let xml_attr_of = function
| `Generated -> Xml.xml_empty "generated" []