X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=97353c3e73cee0c1ba5e710fa368f5c399127d1d;hb=fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60;hp=0dc5dadae51d2b58317098888c3688ba48e10319;hpb=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git

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