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

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index 39fb69b0d..cc13d1ad7 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -128,3 +128,8 @@ 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