- let new_coercions =
- HExtlib.filter_map (
- fun (src, l , tgt) ->
- try
- (match l with
- | [] -> assert false
- | he :: tl ->
- let first_step =
- Cic.Constant ("",
- Some (CoercDb.term_of_carr (CoercDb.Uri he)),
- Cic.Sort Cic.Prop, [], obj_attrs)
- in
- let o,_ =
- List.fold_left (fun (o,univ) coer ->
- match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure rt c
- (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+ try
+ let new_coercions =
+ HExtlib.filter_map (
+ fun (src, l , tgt) ->
+ try
+ (match l with
+ | [] -> assert false
+ | he :: tl ->
+ let first_step =
+ Cic.Constant ("",
+ Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+ Cic.Sort Cic.Prop, [], obj_attrs)
+ in
+ let o,_ =
+ List.fold_left (fun (o,univ) coer ->
+ match o with
+ | Cic.Constant (_,Some c,_,[],_) ->
+ generate_composite_closure rt c
+ (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+ | _ -> assert false
+ ) (first_step, CicUniv.empty_ugraph) tl
+ in
+ let name_src = CoercDb.name_of_carr src in
+ let name_tgt = CoercDb.name_of_carr tgt in
+ let by = List.map UriManager.name_of_uri l in
+ let name = mangle name_tgt name_src by in
+ let buri = UriManager.buri_of_uri uri in
+ let c_uri = number_if_already_defined buri name in
+ let named_obj =
+ match o with
+ | Cic.Constant (_,bo,ty,vl,attrs) ->
+ Cic.Constant (name,bo,ty,vl,attrs)