split into two major parts:

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e0e0bfca3385ec92996bd07da6ad0a4c4b8be674..b62f4b6245dbc5b88b73df47bc8ab77633277f49 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -556,9 +556,9 @@ let decompose_uris_choice_callback uris =
     ) 
 ;;
 
-let mk_fresh_name_callback context name ~typ =
+let mk_fresh_name_callback metasenv context name ~typ =
  let fresh_name =
-  match ProofEngineHelpers.mk_fresh_name context name ~typ with
+  match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
      Cic.Name fresh_name -> fresh_name
    | Cic.Anonymous -> assert false
  in
@@ -1081,7 +1081,7 @@ exception AmbiguousInput;;
 
 (* A WIDGET TO ENTER CIC TERMS *)
 
-module Callbacks =
+module DisambiguateCallbacks =
  struct
   let output_html ?append_NL = output_html ?append_NL (outputhtml ())
   let interactive_user_uri_choice =
@@ -1093,7 +1093,7 @@ module Callbacks =
  end
 ;;
 
-module TermEditor' = ChosenTermEditor.Make(Callbacks);;
+module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);;
 
 (* OTHER FUNCTIONS *)