From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jul 2005 16:14:05 +0000 (+0000)
Subject: mk_fresh_name now returns [name] instead of its basename if [name] is unused
X-Git-Tag: V_0_7_1~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1dc0607346311c1ec5261022cd0f83be1a1ac73;hp=faa5dd9616d34b5ceb30ad693dcfdc34479d4a5e;p=helm.git

mk_fresh_name now returns [name] instead of its basename if [name] is unused
in the context
---

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
 ;;