fresh_name_generator has now also the metasenv parameter.

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

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 200e50a15535eb69da4044fbc7f766eab9399e0c..a304e7e3b27efb8005e32f0cd3e96bacc7ddb7ba 100644 (file)
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -60,8 +60,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
 
 module type Tactics =