| he::tl ->
let tyname = string_of_attr (he#attribute "name")
and inductive = bool_of_attr (he#attribute "inductive")
+ and xid = string_of_attr (he#attribute "id")
and (arity,cons) =
get_names_arity_constructors (he#sub_nodes)
in
- (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
+ (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
;;
(* This is the main function and also the only one used directly from *)
let nbodytype = nbody'#node_type in
match nbodytype with
D.T_element "ConstantBody" ->
+(*CSC: the attribute "for" is ignored and not checked
let for_ = string_of_attr (nbody'#attribute "for") in
+*)
let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
let xidbody = string_of_attr (nbody'#attribute "id") in
let value = (get_content nbody')#extension#to_cic_term [] in
- if paramsbody = params &&
- U.eq (U.uri_of_string for_) !CicParser3.current_uri
- then
+ if paramsbody = params then
C.AConstant (xid, Some xidbody, name, Some value, typ, params)
else
raise (IllFormedXml 6)
| D.T_element "CurrentProof" ->
+(*CSC: the attribute "of" is ignored and not checked
let for_ = string_of_attr (nbody'#attribute "of") in
+*)
let xidbody = string_of_attr (nbody'#attribute "id") in
- let value = (get_content nbody')#extension#to_cic_term [] in
let sons = nbody'#sub_nodes in
let (conjs, value) = get_conjs_value sons in
- if U.eq (U.uri_of_string for_) !CicParser3.current_uri then
- C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
- else
- raise (IllFormedXml 6)
+ C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 6)