X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2Fcic2Xml.ml;h=31765f0552e8005d3c9168138a981026514dd38a;hb=ece1b63a7eec3567ef9eda9bcd1550655a575d07;hp=95f92346bcdb066e24ea9f979a8274f294cc77a8;hpb=ba48c24f4edb0701a0aa346466f2a4211f719ab2;p=helm.git diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml index 95f92346b..31765f055 100644 --- a/components/cic_acic/cic2Xml.ml +++ b/components/cic_acic/cic2Xml.ml @@ -269,7 +269,8 @@ let print_term ?ids_to_inner_sorts = 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 @@ -279,9 +280,13 @@ let xml_of_attrs attributes = | `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"]