mk_fresh_name moved to FreshNamesGenerator.

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2b9e101ab43a11e20db3f22351b57ebf61f317fd..81f9acd666ed8be82a217d2cc6aa56f7ff4d3a3d 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -558,7 +558,7 @@ let decompose_uris_choice_callback uris =
 
 let mk_fresh_name_callback context name ~typ =
  let fresh_name =
-  match ProofEngineHelpers.mk_fresh_name context name ~typ with
+  match FreshNamesGenerator.mk_fresh_name context name ~typ with
      Cic.Name fresh_name -> fresh_name
    | Cic.Anonymous -> assert false
  in