version 0.7.1

[helm.git] / helm / ocaml / cic_unification / freshNamesGenerator.ml

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 0dc5dadae51d2b58317098888c3688ba48e10319..97353c3e73cee0c1ba5e710fa368f5c399127d1d 100644 (file)
--- 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
 ;;