+let saturate_coercion ul metasenv subst context =
+ let cl =
+ List.map
+ (fun u,saturations ->
+ let t = CicUtil.term_of_uri u in
+ let arity =
+ match CoercDb.is_a_coercion t with
+ | Some (_,CoercDb.Fun i,_,_,_) -> i
+ | _ -> 0
+ in
+ arity,t,saturations) ul
+ in
+ let freshmeta = CicMkImplicit.new_meta metasenv subst in
+ List.map
+ (fun (arity,c,saturations) ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context c
+ CicUniv.oblivion_ugraph in
+ let _,metasenv,args,lastmeta =
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ ) cl
+;;
+