[< X.xml_nempty "source" [] (aux s) ;
X.xml_nempty "target" ["binder",id] (aux t)
>]
+ | C.ALetIn (xid,_,C.Anonimous,s,t) ->
+ assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+ | C.ALetIn (xid,_,C.Name id,s,t) ->
+ X.xml_nempty "LETIN" ["id",xid]
+ [< X.xml_nempty "term" [] (aux s) ;
+ X.xml_nempty "letintarget" ["binder",id] (aux t)
+ >]
| C.AAppl (id,_,li) ->
X.xml_nempty "APPLY" ["id",id]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
["name",id ; "params",(encode (List.rev params)) ; "id",xid]
[< X.xml_nempty "type" [] (print_term curi ty) >]
>]
- | C.AVariable (xid, _, name, ty) ->
+ | C.AVariable (xid, _, name, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Variable" ["name",name ; "id",xid]
- [< X.xml_nempty "type" [] (print_term curi ty) >]
+ [< (match bo with
+ None -> [<>]
+ | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
+ ) ;
+ X.xml_nempty "type" [] (print_term curi ty)
+ >]
>]
| C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;