X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=97353c3e73cee0c1ba5e710fa368f5c399127d1d;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=1a94c318599e2678e0898618d1fe40c254653d4b;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 1a94c3185..97353c3e7 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -23,18 +23,23 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let debug_print = fun _ -> ()
+
 (* mk_fresh_name context name typ                      *)
 (* returns an identifier which is fresh in the context *)
 (* and that resembles [name] as much as possible.      *)
 (* [typ] will be the type of the variable              *)
-let mk_fresh_name metasenv context name ~typ =
+let mk_fresh_name ~subst metasenv context name ~typ =
  let module C = Cic in
   let basename =
    match name with
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' metasenv context typ with
+        let ty,_ = 
+          CicTypeChecker.type_of_aux' ~subst metasenv context typ 
+            CicUniv.empty_ugraph in 
+         (match ty with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"
@@ -46,17 +51,19 @@ let mk_fresh_name 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
 ;;
@@ -108,7 +115,7 @@ let clean_dummy_dependent_types t =
             C.Anonymous ->
              if List.mem k rels2 then
 (
-              prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+              debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
               C.Anonymous
 )
              else