- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
- (print_term curi ids_to_inner_sorts t)
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
+ [< List.fold_left
+ (fun i (hid,t) ->
+ [< (match t with
+ Some (n,C.ADecl t) ->
+ X.xml_nempty "Decl"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
+ (print_term curi ids_to_inner_sorts t)
+ | Some (n,C.ADef t) ->
+ X.xml_nempty "Def"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
+ (print_term curi ids_to_inner_sorts t)
+ | None -> X.xml_empty "Hidden" ["id",hid]
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term curi ids_to_inner_sorts t)
+ >]