mk_fresh_name moved to FreshNamesGenerator.

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 5c187b05367c92eecd6241b4db3378531b245fc1..2b505b79de725cdb87974c4d4d8622d3773f7fb6 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -115,7 +115,7 @@ let eta_expand metasenv context t arg =
     T.type_of_aux' metasenv context arg
    in
     let fresh_name =
-     ProofEngineHelpers.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
+     FreshNamesGenerator.mk_fresh_name context (Cic.Name "Heta") ~typ:argty
     in
      (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
 
@@ -312,7 +312,7 @@ let apply_tac ~term ~status =
     raise (Fail (Printexc.to_string e))
 
 let intros_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name) ()
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
  ~status:(proof, goal)
 =
  let module C = Cic in
@@ -329,7 +329,7 @@ let intros_tac
       (newproof, [newmeta])
 
 let cut_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  term ~status:(proof, goal)
 =
  let module C = Cic in
@@ -361,7 +361,7 @@ let cut_tac
       (newproof, [newmeta1 ; newmeta2])
 
 let letin_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  term ~status:(proof, goal)
 =
  let module C = Cic in