let class_of = function
| `Coercion n ->
Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
let class_of = function
| `Coercion n ->
Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
match obj with
C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
match obj with
C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
let xml_for_current_proof_body =
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
(*CSC: I think so. Not implemented yet. *)
let xml_for_current_proof_body =
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
(*CSC: I think so. Not implemented yet. *)
xmlty, Some xmlbo
| C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
xmlty, Some xmlbo
| C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
xmlty, xmlbo
| C.AVariable (id,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
xmlty, xmlbo
| C.AVariable (id,n,bo,ty,params,obj_attrs) ->
let params' = param_attribute_of_params params in
aobj, None
| C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
let params' = param_attribute_of_params params in
aobj, None
| C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
let params' = param_attribute_of_params params in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;