fresh_name_generator has now also the metasenv parameter.

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

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index e4a9fa2e96d8cf991a64a4ee0641093242735821..2b0e58d214328d4a7e7c18b5600658a9ac4e283f 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,8 +62,7 @@ module type Callbacks =
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
-    val mk_fresh_name_callback :
-      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
   end
 ;;