Optional callbacks have been added to tactics that need to introduce

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index de0b375960ffa6fe190e40576cb2da849b42b088..a1e4d21b61078b4c95c2bb03de597b6ea8f01ec5 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -23,7 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val fresh_name : Cic.name -> string
+(* mk_fresh_name context name typ                      *)
+(* returns an identifier which is fresh in the context *)
+(* and that resembles [name] as much as possible.      *)
+(* [typ] will be the type of the variable              *)
+val mk_fresh_name : ProofEngineTypes.mk_fresh_name_type
 
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)