+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+ Cic.Fix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,idx,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n-1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.Fix (n-1,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ (add_single_obj uri obj refinement_toolkit;
+ (n-1,uri::uris)))
+ funs (List.length funs,[]))
+ | Cic.CoFix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n-1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.CoFix (n-1,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n-1,uri::uris)
+ ) funs (List.length funs,[]))
+ | _ -> assert false
+