From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 14 Mar 2003 18:45:41 +0000 (+0000)
Subject: Comment fixed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3b863935bfacffb76ccc913c737be53b840ffe4;p=helm.git

Comment fixed.
---

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index a1e4d21b6..0e2244f43 100644
--- 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