X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=23c3a9b68446a3812f8682a7c2a0e96c78051ac4;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=353ef1f7496082b445329372061f59c56ce83d06;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 353ef1f74..23c3a9b68 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -38,7 +38,7 @@ let print_ann i2a id = let ann = get_ann i2a id in match ann with None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + | Some ann -> (X.xml_nempty "Annotation" [None,"of", id] (X.xml_cdata ann)) ;; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) @@ -106,7 +106,7 @@ let pp_annotation obj i2a curi = [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Annotations" - ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] + [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] begin match obj with C.AConstant (xid, xidobj, _, te, ty, _) ->