mk_fresh_name moved to FreshNamesGenerator.

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ccac132ef6b631b46504d9e63b96c1af5ed8804c..aec43abc373750a42f8edbe26c807950e68d516b 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,44 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* 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 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' [] context typ with
-             C.Sort C.Prop -> "H"
-          | C.Sort C.CProp -> "H"
-           | C.Sort C.Set -> "x"
-           | _ -> "H"
-         )
-        with CicTypeChecker.TypeCheckerFailure _ -> "H"
-       )
-    | C.Name name ->
-       Str.global_replace (Str.regexp "[0-9]*$") "" name
-  in
-   let already_used name =
-    List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
-   in
-    if not (already_used basename) then
-     C.Name basename
-    else
-     let rec try_next n =
-      let name' = basename ^ string_of_int n in
-       if already_used name' then
-        try_next (n+1)
-       else
-        C.Name name'
-     in
-      try_next 1
-;;
-
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
   CicMkImplicit.new_meta metasenv