X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=b62f4b6245dbc5b88b73df47bc8ab77633277f49;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=81f9acd666ed8be82a217d2cc6aa56f7ff4d3a3d;hpb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 81f9acd66..b62f4b624 100644
--- 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 FreshNamesGenerator.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