The fresh_name generator has been moved to ProofEngineHelpers.

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

diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli
index c5593235c79b593f7cfa0078f256ada8d1f84849..de0b375960ffa6fe190e40576cb2da849b42b088 100644 (file)
--- a/helm/gTopLevel/proofEngineHelpers.mli
+++ b/helm/gTopLevel/proofEngineHelpers.mli
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+val fresh_name : Cic.name -> string
+
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)