(* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
(* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_empty "CONST"
["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_empty "CONST"
["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
| C.AMutInd (id,uri,_,i) ->
X.xml_empty "MUTIND"
["uri", (U.string_of_uri uri) ;
| C.AMutInd (id,uri,_,i) ->
X.xml_empty "MUTIND"
["uri", (U.string_of_uri uri) ;
C.ACurrentProof (id,n,conjectures,bo,ty) ->
X.xml_nempty "CurrentProof" ["name",n ; "id", id]
[< List.fold_left
C.ACurrentProof (id,n,conjectures,bo,ty) ->
X.xml_nempty "CurrentProof" ["name",n ; "id", id]
[< List.fold_left
- X.xml_nempty "Conjecture" ["no",(string_of_int n)]
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])
- C.Name n' -> ["name",n']
- | C.Anonimous -> [])
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonimous -> ["id",hid])