- ignore(already_in_obj src_carr tgt_carr uri
- (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)));
- List.iter
- (fun (src,tgt,uri,saturations,_,_,cpos) ->
- CoercDb.add_coercion (src,tgt,uri,saturations,cpos))
- new_coercions;
+ let lemmas =
+ List.fold_left
+ (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
+ let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
+ acc)
+ [] new_coercions
+ in