(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module Y = Entity (* internal functions *******************************************************) let rec rename ns n = let token, mode = n in let n = token ^ "_", mode in if List.mem n ns then rename ns n else n let alpha_name acc attr = let ns, a = acc in match attr with | Y.Name n -> if List.mem n ns then let n = rename ns n in n :: ns, Y.Name n :: a else n :: ns, attr :: a | _ -> assert false (* interface functions ******************************************************) let alpha ns a = let f a names = let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in List.rev_append a names in Y.get_names f a