From e1dc0607346311c1ec5261022cd0f83be1a1ac73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Jul 2005 16:14:05 +0000 Subject: [PATCH] mk_fresh_name now returns [name] instead of its basename if [name] is unused in the context --- helm/ocaml/cic_unification/freshNamesGenerator.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index 0dc5dadae..97353c3e7 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -51,17 +51,19 @@ let mk_fresh_name ~subst metasenv context name ~typ = Str.global_replace (Str.regexp "[0-9]*$") "" name in let already_used name = - List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context + List.exists (function Some (n,_) -> n=name | _ -> false) context in - if not (already_used basename) then + if name <> C.Anonymous && not (already_used name) then + name + else if not (already_used (C.Name basename)) then C.Name basename else let rec try_next n = - let name' = basename ^ string_of_int n in + let name' = C.Name (basename ^ string_of_int n) in if already_used name' then try_next (n+1) else - C.Name name' + name' in try_next 1 ;; -- 2.39.2