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) *)
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\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, _) ->
+ C.AConstant (xid, xidobj, _, te, ty, _, _) ->
[< print_ann i2a xid ;
(match xidobj,te with
Some xidobj, Some te ->
) ;
print_term i2a ty
>]
- | C.AVariable (xid, _, bo, ty,_) ->
+ | C.AVariable (xid, _, bo, ty,_, _) ->
[< print_ann i2a xid ;
(match bo with
None -> [<>]
) ;
print_term i2a ty
>]
- | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) ->
+ | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) ->
[< print_ann i2a xid ;
print_ann i2a xidobj ;
List.fold_right
print_term i2a bo ;
print_term i2a ty
>]
- | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+ | C.AInductiveDefinition (xid, tys, params, paramsno, _) ->
[< print_ann i2a xid ;
List.fold_right
(fun x i -> [< print_mutual_inductive_type i2a x ; i >])