- ProofEngineHelpers: namer_of moved to GrafiteEngine

[helm.git] / components / tactics / proofEngineHelpers.mli

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2..39fb69b0d1067370a408c62be07cc495331516c1 100644 (file)
--- 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