mk_fresh_name moved to FreshNamesGenerator.

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 04959e6962fdc2bd246db1282ae516682e5c837b..28acd57ec250400b5144b5098999b68cca72e412 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -59,7 +59,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  terms ~status:((proof,goal) as status)
 =
   let module C = Cic in