Comment fixed.

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index a1e4d21b61078b4c95c2bb03de597b6ea8f01ec5..0e2244f430d789c66580e03a03b3c27444204708 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -30,8 +30,8 @@
 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