+
+(** 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