Comment fixed.

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index de0b375960ffa6fe190e40576cb2da849b42b088..0e2244f430d789c66580e03a03b3c27444204708 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -23,11 +23,15 @@
  * 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] *)
-(* where n = List.length [canonical_context]                             *)
+(* returns the identity relocation list, which is the list               *)
+(* [Rel 1 ; ... ; Rel n] where n = List.length [canonical_context]       *)
 val identity_relocation_list_for_metavariable :
   'a option list -> Cic.term option list