C.ACurrentProof (id,n,conjectures,bo,ty) ->
X.xml_nempty "CurrentProof" ["name",n ; "id", id]
[< List.fold_left
- (fun i (n,canonical_context,t) ->
+ (fun i (cid,n,canonical_context,t) ->
[< i ;
- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
[< List.fold_left
- (fun i t ->
+ (fun i (hid,t) ->
[< (match t with
Some (n,C.ADecl t) ->
X.xml_nempty "Decl"
(match n with
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
+ 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' -> ["name",n']
- | C.Anonimous -> [])
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
(print_term curi ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" []
+ | None -> X.xml_empty "Hidden" ["id",hid]
) ;
i
>]