HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj, innertypes =
+ let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
if Helm_registry.get_bool "matita.system" then
- let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+ let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
Cic2acic.acic_object_of_cic_object obj
in
let innertypesxml =
Cic2Xml.print_inner_types
uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
in
- annobj, Some innertypesxml
+ annobj, Some innertypesxml, Some ids_to_inner_sorts, false
else
let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
- annobj, None
+ annobj, None, None, true
in
(* prepare XML *)
let xml, bodyxml =
Cic2Xml.print_object
- uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
+ uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ ~generate_attributes annobj
in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
baseuri
in
let new_coercions =
- List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj))
+ List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
new_coercions
in
- let composite_uris = List.map (fun (_,_,uri,_,_) -> uri) new_coercions in
+ let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
(* update the DB *)
List.iter
- (fun (src,tgt,uri,saturations,_) ->
+ (fun (src,tgt,uri,saturations,_,_) ->
CoercDb.add_coercion (src,tgt,uri,saturations))
new_coercions;
CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
let lemmas =
if add_composites then
List.fold_left
- (fun acc (_,tgt,uri,saturations,obj) ->
+ (fun acc (_,tgt,uri,saturations,obj,arity) ->
add_single_obj uri obj refinement_toolkit;
- let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
(uri,arity,saturations)::acc)
[] new_coercions
else