X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.mli;h=39fb69b0d1067370a408c62be07cc495331516c1;hb=5c0c5980586c1fc530fd304275607dd2f8afeba0;hp=cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2;hpb=ae98f5490e20dd26ece5804d9847acfba0e4d16b;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index cc13d1ad7..39fb69b0d 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -128,8 +128,3 @@ val split_with_whd: Cic.context * Cic.term ->
                     (Cic.context * Cic.term) list * int
 val split_with_normalize: Cic.context * Cic.term -> 
                           (Cic.context * Cic.term) list * int
-
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type